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