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

proof

let x be set ; :: 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