let T be non empty TopSpace; :: thesis: for F being Subset-Family of T holds 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 ) }
let F be Subset-Family of T; :: thesis: 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 ) }
set P = { A where A is Subset of T : ex B being Subset of T st
( A = Int (Cl (Int B)) & B in F ) } ;
{ A where A is Subset of T : ex B being Subset of T st
( A = Int (Cl (Int B)) & B in F ) } c= bool the carrier of T

proof

now

let C be set ; :: thesis: ( C in { A where A is Subset of T : ex B being Subset of T st
( A = Int (Cl (Int B)) & B in F ) } implies C in bool the carrier of T )
assume C in { A where A is Subset of T : ex B being Subset of T st
( A = Int (Cl (Int B)) & B in F ) } ; :: thesis: C in bool the carrier of T
then ex A being Subset of T st
( C = A & ex B being Subset of T st
( A = Int (Cl (Int B)) & B in F ) ) ;
hence C in bool the carrier of T ; :: thesis: verum

end;

hence { A where A is Subset of T : ex B being Subset of T st
( A = Int (Cl (Int B)) & B in F ) } c= bool the carrier of T by TARSKI:def 3; :: thesis: verum

end;

then reconsider P = { 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 ;
reconsider P = P as Subset-Family of T ;
for X being set holds
( X in Int (Cl (Int F)) iff X in P )

proof

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

A1: now

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

end;

now

assume A7: X in P ; :: thesis: X in 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 = Int (Cl (Int B)) & B in F ) ) by A7;
then consider B being Subset of T such that
A8: C = Int (Cl (Int B)) and
A9: B in F ;
Int B in Int F by A9, Def1;
then Cl (Int B) in Cl (Int F) by PCOMPS_1:def 3;
hence X in Int (Cl (Int F)) by A8, Def1; :: thesis: verum

end;

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

end;

hence 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 TARSKI:2; :: thesis: verum