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)
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 Th32;
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 ;
A1: Int (Cl (Int (Cl F))) = Int H by Th32;
A2: 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 Th31;
for X being object holds
( X in Int (Cl (Int (Cl F))) iff X in Int (Cl F) )

proof

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

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

assume A4: 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 A2, A4;
then consider B being Subset of T such that
A5: C = Int (Cl B) and
A6: B in F ;
Cl B in Cl F by A6, PCOMPS_1:def 2;
then Int (Cl B) in Int (Cl F) by Def1;
then A7: Cl (Int (Cl B)) in Cl (Int (Cl F)) by PCOMPS_1:def 2;
C = Int (Cl (Int (Cl B))) by A5, TDLAT_1:5;
hence X in Int (Cl (Int (Cl F))) by A7, Def1; :: thesis: verum

end;

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

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