let I be BinOp of [.0,1.]; ( I is satisfying_(EP) & I is satisfying_(OP) implies ( I is satisfying_(I1) & I is satisfying_(I3) & I is satisfying_(I4) & I is satisfying_(I5) & I is satisfying_(LB) & I is satisfying_(RB) & I is satisfying_(NC) & I is satisfying_(NP) & I is satisfying_(IP) ) )
assume AA:
( I is satisfying_(EP) & I is satisfying_(OP) )
; ( I is satisfying_(I1) & I is satisfying_(I3) & I is satisfying_(I4) & I is satisfying_(I5) & I is satisfying_(LB) & I is satisfying_(RB) & I is satisfying_(NC) & I is satisfying_(NP) & I is satisfying_(IP) )
tt:
for x1, x2, y being Element of [.0,1.] st x1 <= x2 holds
I . (x1,y) >= I . (x2,y)
proof
let x1,
x2,
y be
Element of
[.0,1.];
( x1 <= x2 implies I . (x1,y) >= I . (x2,y) )
assume Z1:
x1 <= x2
;
I . (x1,y) >= I . (x2,y)
I . (
x2,
(I . ((I . (x2,y)),y))) =
I . (
(I . (x2,y)),
(I . (x2,y)))
by AA
.=
1
by AA
;
then
x2 <= I . (
(I . (x2,y)),
y)
by AA;
then 1 =
I . (
x1,
(I . ((I . (x2,y)),y)))
by AA, Z1, XXREAL_0:2
.=
I . (
(I . (x2,y)),
(I . (x1,y)))
by AA
;
hence
I . (
x1,
y)
>= I . (
x2,
y)
by AA;
verum
end;
for y being Element of [.0,1.] holds I . (1,y) = y
proof
let y be
Element of
[.0,1.];
I . (1,y) = y
S1:
1
in [.0,1.]
by XXREAL_1:1;
reconsider i = 1 as
Element of
[.0,1.] by XXREAL_1:1;
S2:
I . (
i,
y)
in [.0,1.]
;
I . (
y,
(I . (1,y))) =
I . (1,
(I . (y,y)))
by S1, AA
.=
I . (1,1)
by AA
.=
1
by S1, AA
;
then Z1:
y <= I . (1,
y)
by AA, S2;
I . (
i,
(I . ((I . (i,y)),y))) =
I . (
(I . (i,y)),
(I . (i,y)))
by AA
.=
1
by AA
;
then Z2:
1
<= I . (
(I . (i,y)),
y)
by AA;
1
>= I . (
(I . (i,y)),
y)
by XXREAL_1:1;
then
I . (
(I . (i,y)),
y)
= 1
by Z2, XXREAL_0:1;
then
I . (1,
y)
<= y
by AA;
hence
I . (1,
y)
= y
by Z1, XXREAL_0:1;
verum
end;
then
I is satisfying_(NP)
;
hence
( I is satisfying_(I1) & I is satisfying_(I3) & I is satisfying_(I4) & I is satisfying_(I5) & I is satisfying_(LB) & I is satisfying_(RB) & I is satisfying_(NC) & I is satisfying_(NP) & I is satisfying_(IP) )
by AA, tt; verum