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)
.= (a `2) \/ ((b `2) /\ (a `2))
.= a `2 by XBOOLE_1:22 ;
(a \/ (b /\ a)) `1 = (a `1) \/ ((b /\ a) `1)
.= (a `1) \/ ((b `1) /\ (a `1))
.= a `1 by XBOOLE_1:22 ;
hence a \/ (b /\ a) = a by A1, DOMAIN_1:2; :: thesis: verum