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