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

proof

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

A3: now

assume A4: X in Int (Cl (Int (Cl F))) ; :: thesis: X in Int (Cl F)
then reconsider C = X as Subset of T ;
consider B being Subset of T such that
A5: C = Int B and
A6: B in { A where A is Subset of T : ex B being Subset of T st
( A = Cl (Int (Cl B)) & B in F ) } by A2, A4, Def1;
ex S being Subset of T st
( S = B & ex R being Subset of T st
( S = Cl (Int (Cl R)) & R in F ) ) by A6;
then consider D being Subset of T such that
A7: B = Cl (Int (Cl D)) and
A8: D in F ;
A9: C = Int (Cl D) by A5, A7, TDLAT_1:5;
Cl D in Cl F by A8, PCOMPS_1:def 3;
hence X in Int (Cl F) by A9, Def1; :: thesis: verum

end;

now

assume A10: X in Int (Cl F) ; :: thesis: X in Int (Cl (Int (Cl 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 = Int (Cl B) & B in F ) ) by A1, A10;
then consider B being Subset of T such that
A11: C = Int (Cl B) and
A12: B in F ;
A13: C = Int (Cl (Int (Cl B))) by A11, TDLAT_1:5;
Cl B in Cl F by A12, PCOMPS_1:def 3;
then Int (Cl B) in Int (Cl F) by Def1;
then Cl (Int (Cl B)) in Cl (Int (Cl F)) by PCOMPS_1:def 3;
hence X in Int (Cl (Int (Cl F))) by A13, Def1; :: thesis: verum

end;

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

end;

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