environ
vocabularies HIDDEN, XBOOLE_0, RELAT_1, SUBSET_1, TARSKI, FUNCT_5, FUNCT_1, RELAT_2, ORDERS_2, XXREAL_0, ORDINAL2, LATTICE3, BINOP_1, QMAX_1, STRUCT_0, ROBBINS1, WAYBEL_0, YELLOW_0, EQREL_1, WAYBEL_1, LATTICES, OPOSET_1, CARD_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, FUNCT_1, RELAT_1, RELAT_2, FUNCT_2, RELSET_1, PARTFUN1, BINOP_1, DOMAIN_1, FUNCT_5, ORDINAL1, CARD_1, STRUCT_0, ORDERS_2, LATTICE3, ROBBINS1, WAYBEL_0, WAYBEL_1, YELLOW_0, NECKLACE, QMAX_1, PARTIT_2;
definitions RELAT_2, ORDERS_2, NECKLACE, STRUCT_0;
theorems FUNCT_2, LATTICE3, PARTIT_2, RELAT_1, RELAT_2, RELSET_1, TARSKI, WAYBEL_0, WAYBEL_1, YELLOW_0, ENUMSET1, SYSREL;
schemes ;
registrations XBOOLE_0, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, STRUCT_0, YELLOW_0, WAYBEL24, PARTIT_2, CARD_1, RELAT_2;
constructors HIDDEN, REALSET2, LATTICE3, WAYBEL_1, NECKLACE, QMAX_1, FUNCT_5, PARTIT_2;
requirements HIDDEN, BOOLE, SUBSET, NUMERALS;
equalities RELAT_1, ORDINAL1;
expansions RELAT_2, ORDERS_2, NECKLACE, STRUCT_0;
Lm1:
TrivOrthoRelStr is antisymmetric
;
Lm2:
id {{}} = {[{},{}]}
by SYSREL:13;