let L be non empty Boolean RelStr ; :: thesis: for a, b being Element of L holds
( 'not' (a "\/" b) <= 'not' a & 'not' (a "\/" b) <= 'not' b )
let a, b be Element of L; :: thesis: ( 'not' (a "\/" b) <= 'not' a & 'not' (a "\/" b) <= 'not' b )
( ('not' a) "/\" ('not' b) <= 'not' a & ('not' a) "/\" ('not' b) <= 'not' b ) by YELLOW_0:23;
hence ( 'not' (a "\/" b) <= 'not' a & 'not' (a "\/" b) <= 'not' b ) by Th36; :: thesis: verum