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

UNION ({},F) c= {}

UNION ({},F) c= {}

proof

hence
UNION ({},F) = {}
; :: thesis: verum
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;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