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