environ
vocabularies HIDDEN, SUBSET_1, XBOOLE_0, TARSKI, PRE_TOPC, STRUCT_0, RELAT_1, RCOMP_1, SETFAM_1, CONNSP_1, TSEP_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC, CONNSP_1, BORSUK_1;
definitions PRE_TOPC;
theorems PRE_TOPC, TOPS_1, TOPS_2, CONNSP_1, BORSUK_1, SUBSET_1, XBOOLE_0, XBOOLE_1;
schemes ;
registrations XBOOLE_0, STRUCT_0, PRE_TOPC, TOPS_1, BORSUK_1;
constructors HIDDEN, CONNSP_1, BORSUK_1;
requirements HIDDEN, BOOLE, SUBSET;
equalities SUBSET_1, STRUCT_0;
expansions PRE_TOPC;
Lm1:
for A being set
for B, C, D being Subset of A st B \ C = {} holds
B misses D \ C
Lm2:
for A, B, C being set holds (A /\ B) \ C = (A \ C) /\ (B \ C)
Lm3:
for X being TopStruct
for X0 being SubSpace of X holds TopStruct(# the carrier of X0, the topology of X0 #) is strict SubSpace of X
Lm4:
for T being TopStruct holds TopStruct(# the carrier of T, the topology of T #) is SubSpace of T