let I be set ; :: thesis: for a, b, c being bag of I st a divides b & b divides c holds
a divides c
let a, b, c be bag of I; :: thesis: ( a divides b & b divides c implies a divides c )
assume that
A1: for x being object holds a . x <= b . x and
A2: for x being object holds b . x <= c . x ; :: according to PRE_POLY:def 11 :: thesis: a divides c
let x be object ; :: according to PRE_POLY:def 11 :: thesis: a . x <= c . x
( a . x <= b . x & b . x <= c . x ) by A1, A2;
hence a . x <= c . x by XXREAL_0:2; :: thesis: verum