union F c= D

proof

hence
union F is Subset of D
; :: thesis: verum
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;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