let T be TopSpace; :: thesis: for F being Subset-Family of T holds Cl F = Cl (Cl F)
let F be Subset-Family of T; :: thesis: Cl F = Cl (Cl F)
A1: Cl (Cl F) = { D where D is Subset of T : ex B being Subset of T st
( D = Cl B & B in Cl F ) } by Th7;
A2: Cl F = { A where A is Subset of T : ex B being Subset of T st
( A = Cl B & B in F ) } by Th7;
for X being object holds
( X in Cl F iff X in Cl (Cl F) )

proof

let X be object ; :: thesis: ( X in Cl F iff X in Cl (Cl F) )

A3: now :: thesis: ( X in Cl F implies X in Cl (Cl F) )

assume A4: X in Cl F ; :: thesis: X in Cl (Cl F)
then reconsider C = X as Subset of T ;
consider B being Subset of T such that
A5: C = Cl B and
A6: B in F by A4, PCOMPS_1:def 2;
A7: Cl B in Cl F by A6, PCOMPS_1:def 2;
C = Cl (Cl B) by A5;
hence X in Cl (Cl F) by A1, A7; :: thesis: verum

end;

now :: thesis: ( X in Cl (Cl F) implies X in Cl F )

assume A8: X in Cl (Cl F) ; :: thesis: X in Cl F
then reconsider C = X as Subset of T ;
ex Q being Subset of T st
( Q = C & ex B being Subset of T st
( Q = Cl B & B in Cl F ) ) by A1, A8;
then consider B being Subset of T such that
A9: C = Cl B and
A10: B in Cl F ;
ex Q being Subset of T st
( Q = B & ex R being Subset of T st
( Q = Cl R & R in F ) ) by A2, A10;
hence X in Cl F by A9, PCOMPS_1:def 2; :: thesis: verum

end;

hence ( X in Cl F iff X in Cl (Cl F) ) by A3; :: thesis: verum

end;

hence Cl F = Cl (Cl F) by TARSKI:2; :: thesis: verum