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

proof

assume A2: G is open ; :: thesis: ( G = MaxADSet G & ex G0 being Subset of X0 st
( G0 is open & G0 = G /\ the carrier of X0 ) )
hence G = MaxADSet G by TEX_4:58; :: thesis: ex G0 being Subset of X0 st
( G0 is open & G0 = G /\ the carrier of X0 )
reconsider G0 = G /\ M as Subset of X0 by XBOOLE_1:17;
reconsider G0 = G0 as Subset of X0 ;
take G0 ; :: thesis: ( G0 is open & G0 = G /\ the carrier of X0 )
thus G0 is open by A2, TSP_1:def 1; :: thesis: G0 = G /\ the carrier of X0
thus G0 = G /\ the carrier of X0 ; :: thesis: verum

end;

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

proof

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

proof

let x be set ; :: thesis: ( x in G implies x in MaxADSet E )
assume A8: x in G ; :: thesis: x in MaxADSet E
then reconsider a = x as Point of X ;
{a} c= G by A8, ZFMISC_1:37;
then MaxADSet {a} c= G by A3, TEX_4:36;
then A9: MaxADSet a c= G 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= G by A9, XBOOLE_1:1;
then b in G 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 G c= MaxADSet E by TARSKI:def 3; :: thesis: verum

end;

hence G is open by A3, A6, A7, TEX_4:37; :: thesis: verum