let A, B be non empty preBoolean set ; :: thesis: for a, b being Element of [:A,B:] holds (a \ b) \/ b = a \/ b
let a, b be Element of [:A,B:]; :: thesis: (a \ b) \/ b = a \/ b
( ((a `1) \ (b `1)) \/ (b `1) = (a `1) \/ (b `1) & ((a `2) \ (b `2)) \/ (b `2) = (a `2) \/ (b `2) ) by XBOOLE_1:39;
hence (a \ b) \/ b = a \/ b ; :: thesis: verum