set g = FNegation I;
T0: ( 0 in [.0,1.] & 1 in [.0,1.] ) by XXREAL_1:1;
then T1: (FNegation I) . 0 = I . (0,0) by FNeg
.= 1 by FUZIMPL1:def 3 ;
a1: (FNegation I) . 1 = I . (1,0) by T0, FNeg
.= 0 by FUZIMPL1:def 5 ;
for a, b being Element of [.0,1.] st a <= b holds
(FNegation I) . a >= (FNegation I) . b

proof

let a, b be Element of [.0,1.]; :: thesis: ( a <= b implies (FNegation I) . a >= (FNegation I) . b )
assume Y0: a <= b ; :: thesis: (FNegation I) . a >= (FNegation I) . b
( (FNegation I) . a = I . (a,0) & (FNegation I) . b = I . (b,0) ) by FNeg;
hence (FNegation I) . a >= (FNegation I) . b by Y0, T0, FUZIMPL1:def 1; :: thesis: verum

end;

hence ( FNegation I is satisfying_(N1) & FNegation I is satisfying_(N2) ) by a1, T1, NonInc; :: thesis: verum