let Y be non empty set ; :: thesis: for a, b being Element of Funcs Y,BOOLEAN st a '<' b holds
'not' b '<' 'not' a
let a, b be Element of Funcs 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 15 :: 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 20
.= FALSE ;
then a . x <> TRUE by A1, BVFUNC_1:def 15;
then a . x = FALSE by XBOOLEAN:def 3;
hence ('not' a) . x = 'not' FALSE by MARGREL1:def 20
.= TRUE ;
:: thesis: verum