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;