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;
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

set F0 = F /\ M;
reconsider F0 = F /\ M as Subset of X0 by XBOOLE_1:17;
assume A1: 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:60; :: thesis: ex F0 being Subset of X0 st
( F0 is closed & F0 = F /\ the carrier of X0 )
take F0 ; :: thesis: ( F0 is closed & F0 = F /\ the carrier of X0 )
thus F0 is closed by A1, TSP_1:def 2; :: thesis: F0 = F /\ the carrier of X0
thus F0 = F /\ the carrier of X0 ; :: thesis: verum

end;

assume A2: 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 A3: F0 is closed and
A4: F0 = F /\ the carrier of X0 ; :: thesis: F is closed
set E = F0;
F0 c= M ;
then reconsider E = F0 as Subset of X by XBOOLE_1:1;
A5: E c= MaxADSet F by A2, A4, XBOOLE_1:17;
A6: M is maximal_T_0 by Th11;
for x being object st x in F holds
x in MaxADSet E

proof

let x be object ; :: thesis: ( x in F implies x in MaxADSet E )
assume A7: x in F ; :: thesis: x in MaxADSet E
then reconsider a = x as Point of X ;
consider b being Point of X such that
A8: b in M and
A9: M /\ (MaxADSet a) = {b} by A6;
A10: {b} c= MaxADSet a by A9, XBOOLE_1:17;
{a} c= F by A7, ZFMISC_1:31;
then MaxADSet {a} c= F by A2, TEX_4:34;
then MaxADSet a c= F by TEX_4:28;
then {b} c= F by A10, XBOOLE_1:1;
then b in F by ZFMISC_1:31;
then b in E by A4, A8, XBOOLE_0:def 4;
then {b} c= E by ZFMISC_1:31;
then MaxADSet {b} c= MaxADSet E by TEX_4:31;
then A11: MaxADSet b c= MaxADSet E by TEX_4:28;
b in MaxADSet a by A10, ZFMISC_1:31;
then MaxADSet b = MaxADSet a by TEX_4:21;
then {a} c= MaxADSet b by TEX_4:18;
then a in MaxADSet b by ZFMISC_1:31;
hence x in MaxADSet E by A11; :: thesis: verum

end;

then A12: F c= MaxADSet E by TARSKI:def 3;
MaxADSet E is closed by A3, Th16;
hence F is closed by A2, A5, A12, TEX_4:35; :: thesis: verum