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
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 )
assume A2: F = E ; :: thesis: r " F = MaxADSet E
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
A is maximal_T_0 by Th11;
then A3: A is T_0 by Def4;
set R = { (MaxADSet a) where a is Point of X : a in E } ;
A4: MaxADSet E = union { (MaxADSet a) where a is Point of X : a in E } by TEX_4:def 11;
A5: union { (MaxADSet a) where a is Point of X : a in E } c= r " F

proof

now

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
A6: C = MaxADSet a and
A7: a in E ;

now

let x be set ; :: thesis: ( x in C implies x in r " F )
assume A8: x in C ; :: thesis: x in r " F
then reconsider b = x as Point of X by A6;
A9: MaxADSet a = MaxADSet b by A6, A8, TEX_4:23;
A10: A /\ (MaxADSet a) = {a} by A2, A3, A7, Def2;
A /\ (MaxADSet b) = {(r . b)} by A1, Lm3;
then a = r . x by A9, A10, ZFMISC_1:6;
hence x in r " F by A2, A6, A7, A8, FUNCT_2:46; :: thesis: verum

end;

hence C c= r " F by TARSKI:def 3; :: thesis: verum

end;

hence union { (MaxADSet a) where a is Point of X : a in E } c= r " F by ZFMISC_1:94; :: thesis: verum

end;

r " F c= union { (MaxADSet a) where a is Point of X : a in E }

proof

now

let x be set ; :: thesis: ( x in r " F implies x in union { (MaxADSet a) where a is Point of X : a in E } )
assume A11: 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 ;
A12: r . b in F by A11, FUNCT_2:46;
then reconsider a = r . b as Point of X by A2;
A /\ (MaxADSet b) = {a} by A1, Lm3;
then a in A /\ (MaxADSet b) by ZFMISC_1:37;
then a in MaxADSet b by XBOOLE_0:def 4;
then A13: MaxADSet a = MaxADSet b by TEX_4:23;
MaxADSet a in { (MaxADSet a) where a is Point of X : a in E } by A2, A12;
then A14: MaxADSet a c= union { (MaxADSet a) where a is Point of X : a in E } by ZFMISC_1:92;
{b} c= MaxADSet b by TEX_4:20;
then b in MaxADSet a by A13, ZFMISC_1:37;
hence x in union { (MaxADSet a) where a is Point of X : a in E } by A14; :: thesis: verum

end;

hence r " F c= union { (MaxADSet a) where a is Point of X : a in E } by TARSKI:def 3; :: thesis: verum

end;

hence r " F = MaxADSet E by A4, A5, XBOOLE_0:def 10; :: thesis: verum