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