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

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