reconsider AB = A /\ B as Subset of A by XBOOLE_1:17;
AB is with_non-empty_elements ;
hence A /\ B is with_non-empty_elements ; :: thesis: verum