environ
vocabularies HIDDEN, PRE_TOPC, SUBSET_1, ZFMISC_1, XBOOLE_0, FUNCOP_1, ORDINAL2, FUNCT_1, RELAT_1, STRUCT_0, TOPS_2, T_0TOPSP, RCOMP_1, MCART_1, PARTFUN1, TARSKI, PBOOLE, BORSUK_1, TOPS_1, CONNSP_2, SETFAM_1, FINSET_1, FUNCT_2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, SETFAM_1, FUNCT_1, PBOOLE, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCOP_1, DOMAIN_1, STRUCT_0, PRE_TOPC, TOPS_2, TOPS_1, COMPTS_1, BORSUK_1, T_0TOPSP, FINSET_1, FUNCT_3, CONNSP_2;
definitions TARSKI, TOPS_2, COMPTS_1, T_0TOPSP, FUNCT_1, XBOOLE_0;
theorems BORSUK_1, FUNCOP_1, TOPS_2, FUNCT_2, FUNCT_1, PRE_TOPC, TARSKI, TOPS_1, TOPMETR, ZFMISC_1, CONNSP_2, FUNCT_3, COMPTS_1, FINSET_1, YELLOW12, TSEP_1, TOPGRP_1, XBOOLE_0, XBOOLE_1, SETFAM_1;
schemes PBOOLE, CLASSES1, XFAMILY;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FUNCT_2, STRUCT_0, PRE_TOPC, TOPS_1, BORSUK_1, COMPTS_1, BORSUK_2, ZFMISC_1;
constructors HIDDEN, FUNCT_3, TOPS_1, TOPS_2, COMPTS_1, BORSUK_1, T_0TOPSP, FUNCOP_1, BINOP_1;
requirements HIDDEN, SUBSET, BOOLE;
equalities BINOP_1, STRUCT_0;
expansions TARSKI, TOPS_2, COMPTS_1, T_0TOPSP, XBOOLE_0;
Lm1:
for S being TopStruct holds S,S are_homeomorphic
Lm2:
for S, T being non empty TopStruct st S,T are_homeomorphic holds
T,S are_homeomorphic
Lm3:
for X, Y being non empty TopSpace
for x being Point of X
for Z being non empty Subset of X st Z = {x} holds
[:Y,(X | Z):],Y are_homeomorphic
Lm4:
for X, Y being TopSpace
for Z being Subset of [:Y,X:]
for V being Subset of X st Z = [:([#] Y),V:] holds
TopStruct(# the carrier of [:Y,(X | V):], the topology of [:Y,(X | V):] #) = TopStruct(# the carrier of ([:Y,X:] | Z), the topology of ([:Y,X:] | Z) #)
Lm5:
for T1, T2 being non empty compact TopSpace holds [:T1,T2:] is compact
by Th20;
Lm6:
for X, Y being TopSpace
for XV being SubSpace of X holds [:XV,Y:] is SubSpace of [:X,Y:]