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 consider x1, x2 being set such that
A1: ( x1 in {} & x2 in F & x = x1 \/ x2 ) by SETFAM_1:def 4;
thus x in {} by A1; :: thesis: verum

end;

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