let T be TopSpace; :: thesis: for F being Subset-Family of T holds union (Int F) c= union F
let F be Subset-Family of T; :: thesis: union (Int F) c= union F

now :: thesis: for x being object st x in union (Int F) holds
x in union F

let x be object ; :: thesis: ( x in union (Int F) implies x in union F )
assume x in union (Int F) ; :: thesis: x in union 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 B being set st
( x in B & B in F )

proof

take B ; :: thesis: ( x in B & B in F )
Int B c= B by TOPS_1:16;
hence ( x in B & B in F ) by A1, A3, A4; :: thesis: verum

end;

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

end;

hence union (Int F) c= union F ; :: thesis: verum