A \/ B is with_non-empty_elements

proof

( not {} in A & not {} in B ) by Def9;
hence not {} in A \/ B by XBOOLE_0:def 3; :: according to SETFAM_1:def 9 :: thesis: verum

end;

hence A \/ B is with_non-empty_elements ; :: thesis: verum