( not {} in A & not {} in B ) by Def9;
then not {} in A \/ B by XBOOLE_0:def 3;
hence A \/ B is with_non-empty_elements by Def9; :: thesis: verum