( 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

then not {} in A \/ B by XBOOLE_0:def 3;

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