let n be Ordinal; :: thesis: for b1, b2, b3 being bag of n st b1 divides b2 & b2 divides b3 holds
b1 divides b3
let b1, b2, b3 be bag of n; :: thesis: ( b1 divides b2 & b2 divides b3 implies b1 divides b3 )
assume A1: ( b1 divides b2 & b2 divides b3 ) ; :: thesis: b1 divides b3
now :: thesis: for k being object holds b1 . k <= b3 . k
let k be object ; :: thesis: b1 . k <= b3 . k
( b1 . k <= b2 . k & b2 . k <= b3 . k ) by A1, PRE_POLY:def 11;
hence b1 . k <= b3 . k by XXREAL_0:2; :: thesis: verum
end;
hence b1 divides b3 by PRE_POLY:def 11; :: thesis: verum