environ
vocabularies HIDDEN, XBOOLE_0, PRE_TOPC, SUBSET_1, ZFMISC_1, SETFAM_1, RCOMP_1, TARSKI, STRUCT_0, TOPS_1, TDLAT_3, RELAT_1, TEX_2, TEX_4;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, DOMAIN_1, STRUCT_0, PRE_TOPC, TOPS_1, TOPS_2, BORSUK_1, TSEP_1, TDLAT_3, TEX_2;
definitions TARSKI, XBOOLE_0, STRUCT_0;
theorems TARSKI, SUBSET_1, ZFMISC_1, SETFAM_1, PRE_TOPC, TOPS_1, TOPS_2, PCOMPS_1, TSEP_1, TDLAT_3, TEX_2, XBOOLE_0, XBOOLE_1;
schemes ;
registrations XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC, TOPS_1, BORSUK_1, TSEP_1, TEX_1, TEX_2;
constructors HIDDEN, SETFAM_1, TOPS_1, TOPS_2, REALSET2, BORSUK_1, TSEP_1, TDLAT_3, TEX_1, TEX_2, COMPTS_1;
requirements HIDDEN, BOOLE, SUBSET;
equalities SUBSET_1, STRUCT_0;
expansions TARSKI, XBOOLE_0, SUBSET_1;
Lm1:
for X being non empty TopSpace
for x, y being Point of X st MaxADSet x = MaxADSet y holds
Cl {x} = Cl {y}
Lm2:
for Y being non empty TopStruct
for X1, X2 being SubSpace of Y st the carrier of X1 c= the carrier of X2 holds
X1 is SubSpace of X2
Lm3:
for Y being TopStruct
for A being Subset of Y holds the carrier of (Y | A) = A