let b1, b2 be bag of 1; :: thesis: ( b1 . 0 <= b2 . 0 iff b1 divides b2 )
( b1 . 0 <= b2 . 0 implies b1 divides b2 )

proof

assume A1: b1 . 0 <= b2 . 0 ; :: thesis: b1 divides b2
for k being object st k in 1 holds
b1 . k <= b2 . k

proof

let k be object ; :: thesis: ( k in 1 implies b1 . k <= b2 . k )
assume k in 1 ; :: thesis: b1 . k <= b2 . k
then k = 0 by TARSKI:def 1, CARD_1:49;
hence b1 . k <= b2 . k by A1; :: thesis: verum

end;

hence b1 divides b2 by PRE_POLY:46; :: thesis: verum

end;

hence ( b1 . 0 <= b2 . 0 iff b1 divides b2 ) by PRE_POLY:def 11; :: thesis: verum