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

now :: thesis: for C being object st C in { A where A is Subset of T : ex B being Subset of T st
( A = Cl (Int (Cl B)) & B in F ) } holds
C in bool the carrier of T

let C be object ; :: thesis: ( C in { A where A is Subset of T : ex B being Subset of T st
( A = Cl (Int (Cl 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 = Cl (Int (Cl 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 = Cl (Int (Cl B)) & B in F ) ) ;
hence C in bool the carrier of T ; :: thesis: verum

end;

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

proof

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

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

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

end;

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

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

end;

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

end;

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