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