let X be set ; :: thesis: for b1, b2 being bag of X holds
( b1,b2 are_disjoint iff lcm (b1,b2) = b1 + b2 )
let b1, b2 be bag of X; :: thesis: ( b1,b2 are_disjoint iff lcm (b1,b2) = b1 + b2 )

A1: now

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

now

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

now

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

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

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

end;

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

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

end;

end;

end;

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

end;

hence b1,b2 are_disjoint by Def3; :: thesis: verum

end;

now

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

now

let k be set ; :: thesis: (b1 + b2) . k = max ((b1 . k),(b2 . k))

now

per cases ( b1 . k = 0 or b2 . k = 0 ) by A4, Def3;

case A5: b1 . k = 0 ; :: thesis: (b1 + b2) . k = max ((b1 . k),(b2 . k))

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

end;

case A6: b2 . k = 0 ; :: thesis: (b1 + b2) . k = max ((b1 . k),(b2 . k))

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

end;

end;

end;

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

end;

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

end;

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