let Y be non empty set ; :: thesis: for a, b being Function of Y,BOOLEAN st a '<' b holds
'not' b '<' 'not' a
let a, b be Function of Y,BOOLEAN; :: thesis: ( a '<' b implies 'not' b '<' 'not' a )
assume A1: a '<' b ; :: thesis: 'not' b '<' 'not' a
let x be Element of Y; :: according to BVFUNC_1:def 12 :: thesis: ( not ('not' b) . x = TRUE or ('not' a) . x = TRUE )
assume A2: ('not' b) . x = TRUE ; :: thesis: ('not' a) . x = TRUE
b . x = ('not' ('not' b)) . x
.= 'not' TRUE by A2, MARGREL1:def 19
.= FALSE ;
then a . x <> TRUE by A1;
then a . x = FALSE by XBOOLEAN:def 3;
hence ('not' a) . x = 'not' FALSE by MARGREL1:def 19
.= TRUE ;
:: thesis: verum