let I be BinOp of [.0,1.]; :: thesis: ( 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) ) ; :: thesis: ( 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)

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; :: thesis: verum

assume AA: ( I is satisfying_(EP) & I is satisfying_(OP) ) ; :: thesis: ( 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

for y being Element of [.0,1.] holds I . (1,y) = y
let x1, x2, y be Element of [.0,1.]; :: thesis: ( x1 <= x2 implies I . (x1,y) >= I . (x2,y) )

assume Z1: x1 <= x2 ; :: thesis: 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; :: thesis: verum

end;assume Z1: x1 <= x2 ; :: thesis: 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; :: thesis: verum

proof

then
I is satisfying_(NP)
;
let y be Element of [.0,1.]; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

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; :: thesis: verum