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

A1: now :: thesis:

assume A2: lcm (b1,b2) = b1 + b2 ; :: thesis:

now :: thesis:

let k be object ; :: thesis:
A3: (lcm (b1,b2)) . k = max ((b1 . k),(b2 . k)) by Def2;

now :: thesis:

per cases ) . k = b1 . k or (b1 + b2) . k = b2 . k ) by A2, A3, XXREAL_0:16;

case (b1 + b2) . k = b1 . k ; :: thesis:

then (b1 . k) + (b2 . k) = (b1 . k) + 0 by PRE_POLY:def 5;
hence b2 . k = 0 ; :: thesis:

end;

case (b1 + b2) . k = b2 . k ; :: thesis:

then (b1 . k) + (b2 . k) = 0 + (b2 . k) by PRE_POLY:def 5;
hence b1 . k = 0 ; :: thesis:

end;

end;

end;

hence ( b1 . k = 0 or b2 . k = 0 ) ; :: thesis:

end;

hence b1,b2 are_disjoint ; :: thesis:

end;

now :: thesis:

assume A4: b1,b2 are_disjoint ; :: thesis:

now :: thesis:

let k be object ; :: thesis:

now :: thesis:

per cases by A4;

case A5: b1 . k = 0 ; :: thesis:

hence (b1 + b2) . k = 0 + (b2 . k) by PRE_POLY:def 5
.= max ((b1 . k),(b2 . k)) by A5, XXREAL_0:def 10 ;
:: thesis:

end;

case A6: b2 . k = 0 ; :: thesis:

hence (b1 + b2) . k = (b1 . k) + 0 by PRE_POLY:def 5
.= max ((b1 . k),(b2 . k)) by A6, XXREAL_0:def 10 ;
:: thesis:

end;

end;

end;

hence (b1 + b2) . k = max ((b1 . k),(b2 . k)) ; :: thesis:

end;

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

end;

hence ( b1,b2 are_disjoint iff lcm (b1,b2) = b1 + b2 ) by A1; :: thesis: