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 Th39
.= ('not' a) "\/" b by WAYBEL_1:90 ; :: thesis: verum