let X be non empty TopSpace; :: thesis: for X0 being maximal_Kolmogorov_subspace of X
for F being Subset of X
for F0 being Subset of X0 st F0 = F holds
( F0 is closed iff ( MaxADSet F is closed & F0 = (MaxADSet F) /\ the carrier of X0 ) )
let X0 be maximal_Kolmogorov_subspace of X; :: thesis: for F being Subset of X
for F0 being Subset of X0 st F0 = F holds
( F0 is closed iff ( MaxADSet F is closed & F0 = (MaxADSet 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: for F0 being Subset of X0 st F0 = F holds
( F0 is closed iff ( MaxADSet F is closed & F0 = (MaxADSet F) /\ the carrier of X0 ) )
let F0 be Subset of X0; :: thesis: ( F0 = F implies ( F0 is closed iff ( MaxADSet F is closed & F0 = (MaxADSet F) /\ the carrier of X0 ) ) )
assume A1: F0 = F ; :: thesis: ( F0 is closed iff ( MaxADSet F is closed & F0 = (MaxADSet F) /\ the carrier of X0 ) )
A2: M is maximal_T_0 by Th11;
thus ( F0 is closed implies ( MaxADSet F is closed & F0 = (MaxADSet F) /\ the carrier of X0 ) ) :: thesis: ( MaxADSet F is closed & F0 = (MaxADSet F) /\ the carrier of X0 implies F0 is closed )
proof
assume F0 is closed ; :: thesis: ( MaxADSet F is closed & F0 = (MaxADSet F) /\ the carrier of X0 )
then A3: ex H being Subset of X st
( H is closed & F0 = H /\ M ) by TSP_1:def 2;
hence MaxADSet F is closed by A2, A1, Th5; :: thesis: F0 = (MaxADSet F) /\ the carrier of X0
thus F0 = (MaxADSet F) /\ the carrier of X0 by A2, A1, A3, Th5; :: thesis: verum
end;
assume A4: MaxADSet F is closed ; :: thesis: ( not F0 = (MaxADSet F) /\ the carrier of X0 or F0 is closed )
assume F0 = (MaxADSet F) /\ the carrier of X0 ; :: thesis: F0 is closed
hence F0 is closed by A4, TSP_1:def 2; :: thesis: verum