environ
vocabularies HIDDEN, XBOOLE_0, PRE_TOPC, SUBSET_1, TMAP_1, RCOMP_1, TARSKI, STRUCT_0, TOPS_1, TOPS_3, ZFMISC_1, SETFAM_1, TDLAT_3, NATTRA_1, COMPTS_1, TEX_1, CARD_1;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, SETFAM_1, DOMAIN_1, CARD_1, STRUCT_0, PRE_TOPC, TOPS_1, TMAP_1, TDLAT_3, TOPS_3, COMPTS_1;
definitions PRE_TOPC, TDLAT_3, STRUCT_0;
theorems TARSKI, SUBSET_1, ZFMISC_1, ENUMSET1, PRE_TOPC, TOPS_1, PCOMPS_1, TMAP_1, TDLAT_3, TOPS_3, XBOOLE_0, XBOOLE_1, TSEP_1;
schemes ;
registrations XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC, TOPS_1, TDLAT_3, TMAP_1, CARD_1;
constructors HIDDEN, SETFAM_1, DOMAIN_1, TOPS_1, COMPTS_1, PCOMPS_1, TDLAT_3, TMAP_1, TOPS_3;
requirements HIDDEN, BOOLE, SUBSET, NUMERALS;
equalities COMPTS_1, SUBSET_1, STRUCT_0, ORDINAL1;
expansions PRE_TOPC, TDLAT_3, STRUCT_0;
Lm1:
for X, Y being set holds
( X c= Y iff X is Subset of Y )
;