let Z be non empty set ; :: thesis: for B1, B2 being bag of Z st B1 divides B2 holds
card B1 <= card B2
let B1, B2 be bag of Z; :: thesis: ( B1 divides B2 implies card B1 <= card B2 )
assume B1 divides B2 ; :: thesis: card B1 <= card B2
then consider B3 being bag of Z such that
A: B2 = B1 + B3 by bag1a;
card B2 = (card B1) + (card B3) by A, UPROOTS:15;
hence card B1 <= card B2 by NAT_1:11; :: thesis: verum