environ
vocabularies HIDDEN, PRE_TOPC, SUBSET_1, TOPS_1, TARSKI, RCOMP_1, XBOOLE_0, SETFAM_1, PCOMPS_1, ZFMISC_1, STRUCT_0, FINSET_1, FINSEQ_1, RELAT_1, NAT_1, XXREAL_0, ARYTM_3, CARD_1, FUNCT_1, TDLAT_1, LATTICES, EQREL_1, PBOOLE, LATTICE3, REWRITE1, TDLAT_2;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, SETFAM_1, STRUCT_0, FUNCT_1, ORDINAL1, NUMBERS, FINSET_1, FINSEQ_1, XCMPLX_0, NAT_1, PRE_TOPC, TOPS_1, TOPS_2, PCOMPS_1, BINOP_1, LATTICES, LATTICE3, TDLAT_1, XXREAL_0;
definitions TARSKI, LATTICE3;
theorems TARSKI, ZFMISC_1, SETFAM_1, FINSEQ_1, FUNCT_1, NAT_1, PRE_TOPC, TOPS_1, TOPS_2, PCOMPS_1, LATTICES, LATTICE2, LATTICE3, TDLAT_1, RELAT_1, XBOOLE_0, XBOOLE_1, XREAL_1;
schemes SUBSET_1, NAT_1;
registrations XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC, TOPS_1, TDLAT_1, XREAL_0, FINSEQ_1, RELAT_1, ORDINAL1, NAT_1;
constructors HIDDEN, SETFAM_1, XXREAL_0, NAT_1, MEMBERED, FINSEQ_1, TOPS_1, TOPS_2, PCOMPS_1, LATTICE3, TDLAT_1, BINOP_1;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities RELAT_1, STRUCT_0;
expansions TARSKI, LATTICE3;