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

proof

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

end;

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