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
A1: (a \ b) `1 = (a `1) \ (b `1) by MCART_1:7;
( ((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 by A1, MCART_1:7; :: thesis: verum