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