environ
vocabularies HIDDEN, FINSEQ_1, PARTFUN1, RELAT_1, NAT_1, FUNCT_2, TARSKI, XBOOLE_0, SUBSET_1, FUNCOP_1, FUNCT_1, STRUCT_0, NUMBERS, INCPROJ, XXREAL_0, UNIALG_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, NAT_1, RELAT_1, FUNCT_1, CARD_3, FINSEQ_1, FINSEQ_2, FUNCOP_1, STRUCT_0, PARTFUN1, XXREAL_0, MARGREL1;
definitions STRUCT_0;
theorems FUNCT_1, PARTFUN1, FINSEQ_1, MARGREL1;
schemes FINSEQ_1;
registrations ORDINAL1, RELSET_1, PARTFUN1, FUNCOP_1, XXREAL_0, STRUCT_0, FUNCT_1, FINSEQ_1, MARGREL1;
constructors HIDDEN, PARTFUN1, FUNCOP_1, XXREAL_0, FINSEQ_2, STRUCT_0, CARD_3, MARGREL1;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET;
equalities ;
expansions ;