environ
vocabularies HIDDEN, XBOOLE_0, ZFMISC_1, SUBSET_1, TARSKI, STRUCT_0, PRE_TOPC, RELAT_1, NATTRA_1, TDLAT_3, RCOMP_1, TOPS_3, TOPS_1, SETFAM_1, FUNCT_1, ORDINAL2, COMPTS_1, TEX_1, BORSUK_1, TEX_2, CARD_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, DOMAIN_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, CARD_1, STRUCT_0, PRE_TOPC, TOPS_1, TOPS_2, BORSUK_1, TSEP_1, TDLAT_3, TOPS_3, COMPTS_1, TEX_1;
definitions PRE_TOPC, XBOOLE_0;
theorems TARSKI, SUBSET_1, ZFMISC_1, FUNCT_2, PRE_TOPC, TOPS_1, TOPS_2, BORSUK_1, TSEP_1, TDLAT_3, TOPS_3, TEX_1, RELSET_1, XBOOLE_0, XBOOLE_1;
schemes FUNCT_1, FUNCT_2;
registrations SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, ZFMISC_1, STRUCT_0, PRE_TOPC, TOPS_1, BORSUK_1, TDLAT_3, TEX_1, CARD_1;
constructors HIDDEN, SETFAM_1, TOPS_1, TOPS_2, COMPTS_1, REALSET2, BORSUK_1, TSEP_1, TDLAT_3, TOPS_3, TEX_1;
requirements HIDDEN, BOOLE, SUBSET, NUMERALS;
equalities XBOOLE_0, COMPTS_1, SUBSET_1, STRUCT_0;
expansions PRE_TOPC, XBOOLE_0, SUBSET_1, STRUCT_0;
Lm3:
for P, Q being set st P c= Q & P <> Q holds
Q \ P <> {}
Lm4:
for X being non empty almost_discrete TopSpace
for X0 being non empty maximal_discrete SubSpace of X
for r being continuous Function of X,X0 st r is being_a_retraction holds
for a being Point of X0
for b being Point of X st a = b holds
Cl {b} c= r " {a}