let T be non empty TopSpace; :: thesis: for F being Subset-Family of T holds Cl (Int (Cl (Int F))) = Cl (Int F)
let F be Subset-Family of T; :: thesis: Cl (Int (Cl (Int F))) = Cl (Int F)
set H = { A where A is Subset of T : ex B being Subset of T st
( A = Int (Cl (Int B)) & B in F ) } ;
Int (Cl (Int F)) = { A where A is Subset of T : ex B being Subset of T st
( A = Int (Cl (Int B)) & B in F ) } by Th33;
then reconsider H = { A where A is Subset of T : ex B being Subset of T st
( A = Int (Cl (Int B)) & B in F ) } as Subset-Family of T ;
A1: Cl (Int (Cl (Int F))) = Cl H by Th33;
A2: Cl (Int F) = { A where A is Subset of T : ex B being Subset of T st
( A = Cl (Int B) & B in F ) } by Th30;
for X being object holds
( X in Cl (Int (Cl (Int F))) iff X in Cl (Int F) )

proof

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

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

assume A4: X in Cl (Int F) ; :: thesis: X in Cl (Int (Cl (Int F)))
then reconsider C = X as Subset of T ;
ex D being Subset of T st
( D = C & ex B being Subset of T st
( D = Cl (Int B) & B in F ) ) by A2, A4;
then consider B being Subset of T such that
A5: C = Cl (Int B) and
A6: B in F ;
Int B in Int F by A6, Def1;
then Cl (Int B) in Cl (Int F) by PCOMPS_1:def 2;
then A7: Int (Cl (Int B)) in Int (Cl (Int F)) by Def1;
C = Cl (Int (Cl (Int B))) by A5, TOPS_1:26;
hence X in Cl (Int (Cl (Int F))) by A7, PCOMPS_1:def 2; :: thesis: verum

end;

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

assume A8: X in Cl (Int (Cl (Int F))) ; :: thesis: X in Cl (Int F)
then reconsider C = X as Subset of T ;
consider B being Subset of T such that
A9: C = Cl B and
A10: B in { A where A is Subset of T : ex B being Subset of T st
( A = Int (Cl (Int B)) & B in F ) } by A1, A8, PCOMPS_1:def 2;
ex S being Subset of T st
( S = B & ex R being Subset of T st
( S = Int (Cl (Int R)) & R in F ) ) by A10;
then consider D being Subset of T such that
A11: B = Int (Cl (Int D)) and
A12: D in F ;
A13: Int D in Int F by A12, Def1;
C = Cl (Int D) by A9, A11, TOPS_1:26;
hence X in Cl (Int F) by A13, PCOMPS_1:def 2; :: thesis: verum

end;

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

end;

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