let A, B be non empty preBoolean set ; :: thesis: for a, b being Element of [:A,B:] holds a \/ (b /\ a) = a
let a, b be Element of [:A,B:]; :: thesis: a \/ (b /\ a) = a
A1: (a \/ (b /\ a)) `2 = (a `2 ) \/ ((b /\ a) `2 ) by MCART_1:7
.= (a `2 ) \/ ((b `2 ) /\ (a `2 )) by MCART_1:7
.= a `2 by XBOOLE_1:22 ;
(a \/ (b /\ a)) `1 = (a `1 ) \/ ((b /\ a) `1 ) by MCART_1:7
.= (a `1 ) \/ ((b `1 ) /\ (a `1 )) by MCART_1:7
.= a `1 by XBOOLE_1:22 ;
hence a \/ (b /\ a) = a by A1, DOMAIN_1:12; :: thesis: verum