let L be non empty reflexive transitive antisymmetric with_suprema with_infima RelStr ; :: thesis: ( L is distributive implies for a, b, c being Element of L holds (a "\/" b) \ c = (a \ c) "\/" (b \ c) )

assume A1: L is distributive ; :: thesis: for a, b, c being Element of L holds (a "\/" b) \ c = (a \ c) "\/" (b \ c)

let a, b, c be Element of L; :: thesis: (a "\/" b) \ c = (a \ c) "\/" (b \ c)

thus (a "\/" b) \ c = (a "\/" b) "/\" ('not' c)

.= (('not' c) "/\" a) "\/" (('not' c) "/\" b) by A1, WAYBEL_1:def 3

.= (a \ c) "\/" (b \ c) ; :: thesis: verum

assume A1: L is distributive ; :: thesis: for a, b, c being Element of L holds (a "\/" b) \ c = (a \ c) "\/" (b \ c)

let a, b, c be Element of L; :: thesis: (a "\/" b) \ c = (a \ c) "\/" (b \ c)

thus (a "\/" b) \ c = (a "\/" b) "/\" ('not' c)

.= (('not' c) "/\" a) "\/" (('not' c) "/\" b) by A1, WAYBEL_1:def 3

.= (a \ c) "\/" (b \ c) ; :: thesis: verum