let E be Element of B; :: thesis: E is X -defined

per cases ( not B is empty or B is empty ) ;

suppose not B is empty ; :: thesis: E is X -defined

then reconsider B = B as non empty Subset of (Bags X) ;
reconsider E = E as Element of B ;
E is bag of X by Def12;
hence E is X -defined ; :: thesis: verum

end;

suppose B is empty ; :: thesis: E is X -defined

then E is empty by SUBSET_1:def 1;
hence E is X -defined by RELAT_1:171; :: thesis: verum

end;

end;