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)

now

thus ((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:4
.= (a `1 ) \/ ((b \/ c) `1 ) by MCART_1:7
.= (a \/ (b \/ c)) `1 by MCART_1:7 ; :: thesis: ((a \/ b) \/ c) `2 = (a \/ (b \/ c)) `2
thus ((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:4
.= (a `2 ) \/ ((b \/ c) `2 ) by MCART_1:7
.= (a \/ (b \/ c)) `2 by MCART_1:7 ; :: thesis: verum

end;

hence (a \/ b) \/ c = a \/ (b \/ c) by DOMAIN_1:12; :: thesis: verum