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' ('not' c))) by Th36
.= a "/\" (('not' b) "\/" c) by WAYBEL_1:87
.= (a \ b) "\/" (a "/\" c) by WAYBEL_1:def 3 ; :: thesis: verum