let X be non empty TopSpace; :: thesis: for X0 being maximal_Kolmogorov_subspace of X
for G being Subset of X
for G0 being Subset of X0 st G0 = G holds
( G0 is open iff ( MaxADSet G is open & G0 = (MaxADSet G) /\ the carrier of X0 ) )
let X0 be maximal_Kolmogorov_subspace of X; :: thesis: for G being Subset of X
for G0 being Subset of X0 st G0 = G holds
( G0 is open iff ( MaxADSet G is open & G0 = (MaxADSet G) /\ the carrier of X0 ) )
let G be Subset of X; :: thesis: for G0 being Subset of X0 st G0 = G holds
( G0 is open iff ( MaxADSet G is open & G0 = (MaxADSet G) /\ the carrier of X0 ) )
let G0 be Subset of X0; :: thesis: ( G0 = G implies ( G0 is open iff ( MaxADSet G is open & G0 = (MaxADSet G) /\ the carrier of X0 ) ) )
reconsider M = the carrier of X0 as Subset of X by Lm1;
assume A1: G0 = G ; :: thesis: ( G0 is open iff ( MaxADSet G is open & G0 = (MaxADSet G) /\ the carrier of X0 ) )
A2: M is maximal_T_0 by Th11;
thus ( G0 is open implies ( MaxADSet G is open & G0 = (MaxADSet G) /\ the carrier of X0 ) ) :: thesis: ( MaxADSet G is open & G0 = (MaxADSet G) /\ the carrier of X0 implies G0 is open )
proof
assume G0 is open ; :: thesis: ( MaxADSet G is open & G0 = (MaxADSet G) /\ the carrier of X0 )
then A3: ex H being Subset of X st
( H is open & G0 = H /\ M ) by TSP_1:def 1;
hence MaxADSet G is open by A2, A1, Th6; :: thesis: G0 = (MaxADSet G) /\ the carrier of X0
thus G0 = (MaxADSet G) /\ the carrier of X0 by A2, A1, A3, Th6; :: thesis: verum
end;
assume A4: MaxADSet G is open ; :: thesis: ( not G0 = (MaxADSet G) /\ the carrier of X0 or G0 is open )
assume G0 = (MaxADSet G) /\ the carrier of X0 ; :: thesis: G0 is open
hence G0 is open by A4, TSP_1:def 1; :: thesis: verum