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