let L be non empty Boolean RelStr ; :: thesis: for a, b, c being Element of L holds a \ (b "/\" c) = (a \ b) "\/" (a \ c)
let a, b, c be Element of L; :: thesis: a \ (b "/\" c) = (a \ b) "\/" (a \ c)
thus a \ (b "/\" c) = a "/\" (('not' b) "\/" ('not' c)) by Th36
.= (a \ b) "\/" (a \ c) by WAYBEL_1:def 3 ; :: thesis: verum