set f = SugenoNegation r;
AA:
r > - 1
by GreatDef;
AB:
( 0 in [.0,1.] & 1 in [.0,1.] )
by XXREAL_1:1;
then AJ: (SugenoNegation r) . 0 =
(1 - 0) / (1 + (r * 0))
by DefSugeno, AA
.=
1
;
(SugenoNegation r) . 1 =
(1 - 1) / (1 + (r * 1))
by DefSugeno, AA, AB
.=
0
;
hence
SugenoNegation r is satisfying_(N1)
by AJ; SugenoNegation r is satisfying_(N2)
for x, y being Element of [.0,1.] st x <= y holds
(SugenoNegation r) . x >= (SugenoNegation r) . y
proof
let x,
y be
Element of
[.0,1.];
( x <= y implies (SugenoNegation r) . x >= (SugenoNegation r) . y )
assume B2:
x <= y
;
(SugenoNegation r) . x >= (SugenoNegation r) . y
set m =
(1 + (r * x)) * (1 + (r * y));
t1:
y - x >= x - x
by B2, XREAL_1:6;
St:
1
+ r > 1
+ (- 1)
by GreatDef, XREAL_1:6;
(
0 <= x &
x <= 1 )
by XXREAL_1:1;
then S2:
1
+ (r * x) > 0
by LemmaImp, GreatDef;
(
0 <= y &
y <= 1 )
by XXREAL_1:1;
then S1:
1
+ (r * y) > 0
by LemmaImp, GreatDef;
R1:
(SugenoNegation r) . x =
(1 - x) / (1 + (r * x))
by DefSugeno, AA
.=
((1 - x) * (1 + (r * y))) / ((1 + (r * x)) * (1 + (r * y)))
by XCMPLX_1:91, S1
;
R2:
(SugenoNegation r) . y =
(1 - y) / (1 + (r * y))
by DefSugeno, AA
.=
((1 - y) * (1 + (r * x))) / ((1 + (r * x)) * (1 + (r * y)))
by XCMPLX_1:91, S2
;
((SugenoNegation r) . x) - ((SugenoNegation r) . y) = ((y - x) * (1 + r)) / ((1 + (r * x)) * (1 + (r * y)))
by R1, R2;
then
(((SugenoNegation r) . x) - ((SugenoNegation r) . y)) + ((SugenoNegation r) . y) >= 0 + ((SugenoNegation r) . y)
by S1, XREAL_1:6, t1, St, S2;
hence
(SugenoNegation r) . x >= (SugenoNegation r) . y
;
verum
end;
hence
SugenoNegation r is satisfying_(N2)
by NonInc; verum