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