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