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 F = { A where A is Subset of T : ex B being Subset of T st
( A = Cl B & B in F ) } by Th7;
A2: 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;
for X being set holds
( X in Cl F iff X in Cl (Cl F) )

proof

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

A3: now

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 3;
( C = Cl (Cl B) & Cl B in Cl F ) by A5, A6, PCOMPS_1:def 3;
hence X in Cl (Cl F) by A2; :: thesis: verum

end;

now

assume A7: 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 A2, A7;
then consider B being Subset of T such that
A8: C = Cl B and
A9: 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 A1, A9;
then consider R being Subset of T such that
A10: B = Cl R and
A11: R in F ;
thus X in Cl F by A8, A10, A11, PCOMPS_1:def 3; :: 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