environ
vocabularies HIDDEN, PRE_TOPC, SUBSET_1, XBOOLE_0, TARSKI, TOPS_1, RCOMP_1, SETFAM_1, ZFMISC_1, STRUCT_0, BINOP_1, FUNCT_1, MCART_1, LATTICES, EQREL_1, REALSET1, NAT_LAT, TDLAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, REALSET1, STRUCT_0, PRE_TOPC, LATTICES, BINOP_1, TOPS_1, FUNCT_1, DOMAIN_1, FUNCT_2, NAT_LAT;
definitions TARSKI, LATTICES, NAT_LAT;
theorems TOPS_1, PRE_TOPC, LATTICE2, BINOP_1, FUNCT_2, SUBSET_1, MCART_1, FUNCT_1, XBOOLE_1, XTUPLE_0, ZFMISC_1;
schemes FUNCT_2, BINOP_2;
registrations SUBSET_1, REALSET1, LATTICES, TOPS_1, RELAT_1, PRE_TOPC;
constructors HIDDEN, PARTFUN1, BINOP_1, REALSET1, TOPS_1, NAT_LAT;
requirements HIDDEN, BOOLE, SUBSET;
equalities LATTICES, XBOOLE_0, BINOP_1, REALSET1, SUBSET_1, STRUCT_0;
expansions TARSKI, XBOOLE_0;