let X be set ; :: thesis: for b1, b2 being bag of X holds

( b2 divides b1 iff lcm (b1,b2) = b1 )

let b1, b2 be bag of X; :: thesis: ( b2 divides b1 iff lcm (b1,b2) = b1 )

( b2 divides b1 iff lcm (b1,b2) = b1 )

let b1, b2 be bag of X; :: thesis: ( b2 divides b1 iff lcm (b1,b2) = b1 )

now :: thesis: ( b2 divides b1 implies lcm (b1,b2) = b1 )

hence
( b2 divides b1 iff lcm (b1,b2) = b1 )
by Th3; :: thesis: verumassume A1:
b2 divides b1
; :: thesis: lcm (b1,b2) = b1

for k being object holds b1 . k = max ((b1 . k),(b2 . k)) by XXREAL_0:def 10, A1, PRE_POLY:def 11;

hence lcm (b1,b2) = b1 by Def2; :: thesis: verum

end;for k being object holds b1 . k = max ((b1 . k),(b2 . k)) by XXREAL_0:def 10, A1, PRE_POLY:def 11;

hence lcm (b1,b2) = b1 by Def2; :: thesis: verum