namespace latin:/algebraic❚
fixmeta latin:/?SFOLEQND❚
theory Set =
universe : tp❙
U = tm universe❙
❚
theory SetHom =
structure domain : ?Set❚
structure codomain : ?Set❚
U : domain/U ⟶ codomain/U ❙
❚
theory SubSet =
structure parent : ?Set =
U # P❙
❚
universe : P ⟶ prop❘# U 1 prec 40❙
❚