let X be non empty TopSpace; :: thesis: 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
let X0 be non empty maximal_Kolmogorov_subspace of X; :: thesis: 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
let r be continuous Function of X,X0; :: thesis: ( r is being_a_retraction implies for E being Subset of X
for F being Subset of X0 st F = E holds
r " F = MaxADSet E )
assume A1: r is being_a_retraction ; :: thesis: for E being Subset of X
for F being Subset of X0 st F = E holds
r " F = MaxADSet E
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
let E be Subset of X; :: thesis: for F being Subset of X0 st F = E holds
r " F = MaxADSet E
let F be Subset of X0; :: thesis: ( F = E implies r " F = MaxADSet E )
set R = { (MaxADSet a) where a is Point of X : a in E } ;
assume A2: F = E ; :: thesis: r " F = MaxADSet E
now :: thesis: for x being object st x in r " F holds
x in union { (MaxADSet a) where a is Point of X : a in E }
let x be object ; :: thesis: ( x in r " F implies x in union { (MaxADSet a) where a is Point of X : a in E } )
assume A3: x in r " F ; :: thesis: x in union { (MaxADSet a) where a is Point of X : a in E }
then reconsider b = x as Point of X ;
A4: r . b in F by A3, FUNCT_2:38;
then reconsider a = r . b as Point of X by A2;
MaxADSet a in { (MaxADSet a) where a is Point of X : a in E } by A2, A4;
then A5: MaxADSet a c= union { (MaxADSet a) where a is Point of X : a in E } by ZFMISC_1:74;
A /\ (MaxADSet b) = {a} by A1, Lm3;
then a in A /\ (MaxADSet b) by ZFMISC_1:31;
then a in MaxADSet b by XBOOLE_0:def 4;
then A6: MaxADSet a = MaxADSet b by TEX_4:21;
{b} c= MaxADSet b by TEX_4:18;
then b in MaxADSet a by A6, ZFMISC_1:31;
hence x in union { (MaxADSet a) where a is Point of X : a in E } by A5; :: thesis: verum
end;
then A7: r " F c= union { (MaxADSet a) where a is Point of X : a in E } by TARSKI:def 3;
A is maximal_T_0 by Th11;
then A8: A is T_0 ;
now :: thesis: for C being set st C in { (MaxADSet a) where a is Point of X : a in E } holds
C c= r " F
let C be set ; :: thesis: ( C in { (MaxADSet a) where a is Point of X : a in E } implies C c= r " F )
assume C in { (MaxADSet a) where a is Point of X : a in E } ; :: thesis: C c= r " F
then consider a being Point of X such that
A9: C = MaxADSet a and
A10: a in E ;
now :: thesis: for x being object st x in C holds
x in r " F
let x be object ; :: thesis: ( x in C implies x in r " F )
assume A11: x in C ; :: thesis: x in r " F
then reconsider b = x as Point of X by A9;
A12: A /\ (MaxADSet b) = {(r . b)} by A1, Lm3;
A13: A /\ (MaxADSet a) = {a} by A2, A8, A10;
MaxADSet a = MaxADSet b by A9, A11, TEX_4:21;
then a = r . x by A13, A12, ZFMISC_1:3;
hence x in r " F by A2, A9, A10, A11, FUNCT_2:38; :: thesis: verum
end;
hence C c= r " F by TARSKI:def 3; :: thesis: verum
end;
then A14: union { (MaxADSet a) where a is Point of X : a in E } c= r " F by ZFMISC_1:76;
MaxADSet E = union { (MaxADSet a) where a is Point of X : a in E } by TEX_4:def 11;
hence r " F = MaxADSet E by A14, A7, XBOOLE_0:def 10; :: thesis: verum