let I be satisfying_(EP) satisfying_(OP) BinOp of [.0,1.]; :: thesis: for x being Element of [.0,1.] holds x <= (FNegation I) . ((FNegation I) . x)
let x be Element of [.0,1.]; :: thesis: x <= (FNegation I) . ((FNegation I) . x)
set f = FNegation I;
A1: 0 in [.0,1.] by XXREAL_1:1;
(FNegation I) . x in [.0,1.] ;
then A2: I . (x,0) in [.0,1.] by FNeg;
then a7: I . (x,(I . ((I . (x,0)),0))) = I . ((I . (x,0)),(I . (x,0))) by A1, FUZIMPL2:def 2
.= 1 by A2, FUZIMPL2:def 3 ;
I . ((I . (x,0)),0) = I . (((FNegation I) . x),0) by FNeg
.= (FNegation I) . ((FNegation I) . x) by FNeg ;
hence x <= (FNegation I) . ((FNegation I) . x) by a7, FUZIMPL2:def 4; :: thesis: verum