environ
vocabularies HIDDEN, XBOOLE_0, PRE_TOPC, SUBSET_1, TEX_4, RCOMP_1, TARSKI, STRUCT_0, TOPS_1, ZFMISC_1, SETFAM_1, FUNCT_1, RELAT_1, NATTRA_1, ORDINAL2, BORSUK_1, TSP_2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, RELAT_1, RELSET_1, FUNCT_2, DOMAIN_1, STRUCT_0, PRE_TOPC, TOPS_1, BORSUK_1, TSEP_1, TEX_2, TEX_3, TEX_4, TSP_1;
definitions ;
theorems TARSKI, ZFMISC_1, FUNCT_1, FUNCT_2, PRE_TOPC, TOPS_1, BORSUK_1, TSEP_1, TOPS_3, TEX_2, TEX_3, TEX_4, TSP_1, RELAT_1, XBOOLE_0, XBOOLE_1, SUBSET_1, RELSET_1;
schemes TEX_2, FUNCT_2;
registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, PRE_TOPC, TOPS_1, TSP_1;
constructors HIDDEN, TOPS_1, BORSUK_1, TSEP_1, TEX_2, TEX_4, TSP_1, TEX_3;
requirements HIDDEN, BOOLE, SUBSET;
equalities SUBSET_1, STRUCT_0, RELAT_1;
expansions SUBSET_1;
Lm2:
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for r being continuous Function of X,X0 st r is being_a_retraction holds
for a being Point of X
for b being Point of X0 st a = b holds
r " (Cl {b}) = Cl {a}
Lm3:
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for r being continuous Function of X,X0 st r is being_a_retraction holds
for A being Subset of X st A = the carrier of X0 holds
for a being Point of X holds A /\ (MaxADSet a) = {(r . a)}
Lm4:
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for r being continuous Function of X,X0 st r is being_a_retraction holds
for a being Point of X
for b being Point of X0 st a = b holds
MaxADSet a c= r " {b}
Lm5:
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for r being continuous Function of X,X0 st r is being_a_retraction holds
for a being Point of X
for b being Point of X0 st a = b holds
r " {b} = MaxADSet a
Lm6:
for X being non empty TopSpace
for X0 being non empty maximal_Kolmogorov_subspace of X
for r being continuous Function of X,X0 st r is being_a_retraction holds
for E being Subset of X
for F being Subset of X0 st F = E holds
r " F = MaxADSet E