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 `1 ) \ (b `1 )) \/ (b `1 ) = (a `1 ) \/ (b `1 ) & ((a `2 ) \ (b `2 )) \/ (b `2 ) = (a `2 ) \/ (b `2 ) ) by XBOOLE_1:39;
( (a \ b) `1 = (a `1 ) \ (b `1 ) & (a \ b) `2 = (a `2 ) \ (b `2 ) ) by MCART_1:7;
hence (a \ b) \/ b = a \/ b by A1; :: thesis: verum