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)
proof
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
.= I . ((I . (x2,y)),(I . (x1,y))) by AA ;
hence I . (x1,y) >= I . (x2,y) by AA; :: thesis: verum
end;
for y being Element of [.0,1.] holds I . (1,y) = y
proof
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 ;
then I . (1,y) <= y by AA;
hence I . (1,y) = y by ; :: thesis: 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; :: thesis: verum