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;
A1: M is maximal_T_0 by Th11;
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 A2: F0 = F ; :: thesis: ( F0 is closed iff ( MaxADSet F is closed & F0 = (MaxADSet F) /\ the carrier of X0 ) )
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 consider H being Subset of X such that
A3: H is closed and
A4: F0 = H /\ M by TSP_1:def 2;
thus MaxADSet F is closed by A1, A2, A3, A4, Th5; :: thesis: F0 = (MaxADSet F) /\ the carrier of X0
thus F0 = (MaxADSet F) /\ the carrier of X0 by A1, A2, A3, A4, Th5; :: thesis: verum

end;

assume A5: 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 A5, TSP_1:def 2; :: thesis: verum