union F c= D
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union F or x in D )
assume x in union F ; :: thesis: x in D
then ex Z being set st
( x in Z & Z in F ) by TARSKI:def 4;
hence x in D ; :: thesis: verum
end;
hence union F is Subset of D ; :: thesis: verum