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 ) ) )
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 ) ) )
reconsider M = the carrier of X0 as Subset of X by Lm1;
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
reconsider G0 = G /\ M as Subset of X0 by XBOOLE_1:17;
reconsider G0 = G0 as Subset of X0 ;
assume A1: 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:56; :: thesis: ex G0 being Subset of X0 st
( G0 is open & G0 = G /\ the carrier of X0 )
take G0 ; :: thesis: ( G0 is open & G0 = G /\ the carrier of X0 )
thus G0 is open by A1, TSP_1:def 1; :: thesis: G0 = G /\ the carrier of X0
thus G0 = G /\ the carrier of X0 ; :: thesis: verum
end;
assume A2: 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 A3: G0 is open and
A4: G0 = G /\ the carrier of X0 ; :: thesis: G is open
set E = G0;
G0 c= M ;
then reconsider E = G0 as Subset of X by XBOOLE_1:1;
A5: E c= MaxADSet G by A2, A4, XBOOLE_1:17;
A6: M is maximal_T_0 by Th11;
for x being object st x in G holds
x in MaxADSet E
proof
let x be object ; :: thesis: ( x in G implies x in MaxADSet E )
assume A7: x in G ; :: 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= G by A7, ZFMISC_1:31;
then MaxADSet {a} c= G by A2, TEX_4:34;
then MaxADSet a c= G by TEX_4:28;
then {b} c= G by A10, XBOOLE_1:1;
then b in G 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: G c= MaxADSet E by TARSKI:def 3;
MaxADSet E is open by A3, Th14;
hence G is open by A2, A5, A12, TEX_4:35; :: thesis: verum