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

proof

take Int (Cl (Int B)) ; :: thesis: ( x in Int (Cl (Int B)) & Int (Cl (Int B)) in Int (Cl (Int F)) )
Int B in Int F by A4, Def1;
then A5: Cl (Int B) in Cl (Int F) by PCOMPS_1:def 2;
A c= Int (Cl (Int B)) by A3, TDLAT_1:4;
hence ( x in Int (Cl (Int B)) & Int (Cl (Int B)) in Int (Cl (Int F)) ) by A1, A5, Def1; :: thesis: verum

end;

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