let T be non empty TopSpace; :: thesis: for F being Subset-Family of T holds union (Cl (Int (Cl F))) c= union (Cl F)
let F be Subset-Family of T; :: thesis: union (Cl (Int (Cl F))) c= union (Cl F)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (Cl (Int (Cl F))) or x in union (Cl F) )
assume x in union (Cl (Int (Cl F))) ; :: thesis: x in union (Cl F)
then consider A being set such that
A1: x in A and
A2: A in Cl (Int (Cl F)) by TARSKI:def 4;
reconsider A = A as Subset of T by A2;
consider B being Subset of T such that
A3: A = Cl B and
A4: B in Int (Cl F) by A2, PCOMPS_1:def 2;
consider D being Subset of T such that
A5: B = Int D and
A6: D in Cl F by A4, Def1;
consider E being Subset of T such that
A7: D = Cl E and
A8: E in F by A6, PCOMPS_1:def 2;
ex P being set st
( x in P & P in Cl F )

proof

take Cl E ; :: thesis: ( x in Cl E & Cl E in Cl F )
A c= Cl E by A3, A5, A7, TDLAT_1:3;
hence ( x in Cl E & Cl E in Cl F ) by A1, A8, PCOMPS_1:def 2; :: thesis: verum

end;

hence x in union (Cl F) by TARSKI:def 4; :: thesis: verum