let F be set ; :: thesis: UNION ({},F) = {}
UNION ({},F) c= {}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in UNION ({},F) or x in {} )
assume x in UNION ({},F) ; :: thesis: x in {}
then ex x1, x2 being set st
( x1 in {} & x2 in F & x = x1 \/ x2 ) by SETFAM_1:def 4;
hence x in {} ; :: thesis: verum

end;

hence UNION ({},F) = {} ; :: thesis: verum