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