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

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