let X be non empty TopSpace; :: thesis: for X0 being maximal_Kolmogorov_subspace of X
for F being Subset of X holds
( F is closed iff ( F = MaxADSet F & ex F0 being Subset of X0 st
( F0 is closed & F0 = F /\ the carrier of X0 ) ) )
let X0 be maximal_Kolmogorov_subspace of X; :: thesis: for F being Subset of X holds
( F is closed iff ( F = MaxADSet F & ex F0 being Subset of X0 st
( F0 is closed & F0 = F /\ the carrier of X0 ) ) )
reconsider M = the carrier of X0 as Subset of X by TSEP_1:1;
A1: M is maximal_T_0 by Th11;
let F be Subset of X; :: thesis: ( F is closed iff ( F = MaxADSet F & ex F0 being Subset of X0 st
( F0 is closed & F0 = F /\ the carrier of X0 ) ) )
thus ( F is closed implies ( F = MaxADSet F & ex F0 being Subset of X0 st
( F0 is closed & F0 = F /\ the carrier of X0 ) ) ) :: thesis: ( F = MaxADSet F & ex F0 being Subset of X0 st
( F0 is closed & F0 = F /\ the carrier of X0 ) implies F is closed )

proof

assume A2: F is closed ; :: thesis: ( F = MaxADSet F & ex F0 being Subset of X0 st
( F0 is closed & F0 = F /\ the carrier of X0 ) )
hence F = MaxADSet F by TEX_4:62; :: thesis: ex F0 being Subset of X0 st
( F0 is closed & F0 = F /\ the carrier of X0 )
set F0 = F /\ M;
reconsider F0 = F /\ M as Subset of X0 by XBOOLE_1:17;
take F0 ; :: thesis: ( F0 is closed & F0 = F /\ the carrier of X0 )
thus F0 is closed by A2, TSP_1:def 2; :: thesis: F0 = F /\ the carrier of X0
thus F0 = F /\ the carrier of X0 ; :: thesis: verum

end;

assume A3: F = MaxADSet F ; :: thesis: ( for F0 being Subset of X0 holds
( not F0 is closed or not F0 = F /\ the carrier of X0 ) or F is closed )
given F0 being Subset of X0 such that A4: F0 is closed and
A5: F0 = F /\ the carrier of X0 ; :: thesis: F is closed
set E = F0;
( F0 c= M & M c= the carrier of X ) ;
then reconsider E = F0 as Subset of X by XBOOLE_1:1;
A6: MaxADSet E is closed by A4, Th16;
A7: E c= MaxADSet F by A3, A5, XBOOLE_1:17;
F c= MaxADSet E

proof

for x being set st x in F holds
x in MaxADSet E

proof

let x be set ; :: thesis: ( x in F implies x in MaxADSet E )
assume A8: x in F ; :: thesis: x in MaxADSet E
then reconsider a = x as Point of X ;
{a} c= F by A8, ZFMISC_1:37;
then MaxADSet {a} c= F by A3, TEX_4:36;
then A9: MaxADSet a c= F by TEX_4:30;
consider b being Point of X such that
A10: b in M and
A11: M /\ (MaxADSet a) = {b} by A1, Def6;
A12: {b} c= MaxADSet a by A11, XBOOLE_1:17;
then {b} c= F by A9, XBOOLE_1:1;
then b in F by ZFMISC_1:37;
then b in E by A5, A10, XBOOLE_0:def 4;
then {b} c= E by ZFMISC_1:37;
then MaxADSet {b} c= MaxADSet E by TEX_4:33;
then A13: MaxADSet b c= MaxADSet E by TEX_4:30;
b in MaxADSet a by A12, ZFMISC_1:37;
then MaxADSet b = MaxADSet a by TEX_4:23;
then {a} c= MaxADSet b by TEX_4:20;
then a in MaxADSet b by ZFMISC_1:37;
hence x in MaxADSet E by A13; :: thesis: verum

end;

hence F c= MaxADSet E by TARSKI:def 3; :: thesis: verum

end;

hence F is closed by A3, A6, A7, TEX_4:37; :: thesis: verum