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