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)
thus a \/ (b /\ c) = (a \/ (c /\ a)) \/ (c /\ b) by Th6
.= a \/ ((c /\ a) \/ (c /\ b)) by Th3
.= a \/ (c /\ (a \/ b)) by Th5
.= ((a \/ b) /\ a) \/ ((a \/ b) /\ c) by Th7
.= (a \/ b) /\ (a \/ c) by Th5 ; :: thesis: verum