set I = I_WB ;
a0: for x being Element of [.0,1.] holds I_WB . (x,x) = 1

proof

let x be Element of [.0,1.]; :: thesis: I_WB . (x,x) = 1
x <= 1 by XXREAL_1:1;

per cases then ( x < 1 or x = 1 ) by XXREAL_0:1;

suppose x < 1 ; :: thesis: I_WB . (x,x) = 1

hence I_WB . (x,x) = 1 by FUZIMPL1:def 22; :: thesis: verum

end;

suppose x = 1 ; :: thesis: I_WB . (x,x) = 1

hence I_WB . (x,x) = 1 by FUZIMPL1:def 22; :: thesis: verum

end;

end;

end;

BB: 1 in [.0,1.] by XXREAL_1:1;
CA: for x, y, z being Element of [.0,1.] holds I_WB . (x,(I_WB . (y,z))) = I_WB . (y,(I_WB . (x,z)))

proof

let x, y, z be Element of [.0,1.]; :: thesis: I_WB . (x,(I_WB . (y,z))) = I_WB . (y,(I_WB . (x,z)))
( x <= 1 & y <= 1 & z <= 1 ) by XXREAL_1:1;

per cases then ( ( x = 1 & y = 1 ) or ( x < 1 & y = 1 ) or ( x = 1 & y < 1 ) or ( x < 1 & y < 1 ) ) by XXREAL_0:1;

suppose Y0: ( x = 1 & y = 1 ) ; :: thesis: I_WB . (x,(I_WB . (y,z))) = I_WB . (y,(I_WB . (x,z)))

then Y1: I_WB . (x,(I_WB . (y,z))) = I_WB . (x,z) by FUZIMPL1:def 22
.= z by FUZIMPL1:def 22, Y0 ;
I_WB . (y,(I_WB . (x,z))) = I_WB . (y,z) by Y0, FUZIMPL1:def 22
.= z by Y0, FUZIMPL1:def 22 ;
hence I_WB . (x,(I_WB . (y,z))) = I_WB . (y,(I_WB . (x,z))) by Y1; :: thesis: verum

end;

suppose Y0: ( x < 1 & y = 1 ) ; :: thesis: I_WB . (x,(I_WB . (y,z))) = I_WB . (y,(I_WB . (x,z)))

then I_WB . (y,(I_WB . (x,z))) = I_WB . (y,1) by FUZIMPL1:def 22
.= 1 by Y0, FUZIMPL1:def 22 ;
hence I_WB . (x,(I_WB . (y,z))) = I_WB . (y,(I_WB . (x,z))) by Y0, FUZIMPL1:def 22; :: thesis: verum

end;

suppose Y0: ( x = 1 & y < 1 ) ; :: thesis: I_WB . (x,(I_WB . (y,z))) = I_WB . (y,(I_WB . (x,z)))

then I_WB . (x,(I_WB . (y,z))) = I_WB . (x,1) by FUZIMPL1:def 22
.= 1 by FUZIMPL1:def 22, Y0 ;
hence I_WB . (x,(I_WB . (y,z))) = I_WB . (y,(I_WB . (x,z))) by Y0, FUZIMPL1:def 22; :: thesis: verum

end;

suppose Y0: ( x < 1 & y < 1 ) ; :: thesis: I_WB . (x,(I_WB . (y,z))) = I_WB . (y,(I_WB . (x,z)))

then I_WB . (x,(I_WB . (y,z))) = 1 by FUZIMPL1:def 22;
hence I_WB . (x,(I_WB . (y,z))) = I_WB . (y,(I_WB . (x,z))) by Y0, FUZIMPL1:def 22; :: thesis: verum

end;

end;

end;

not for x, y being Element of [.0,1.] holds
( I_WB . (x,y) = 1 iff x <= y )

proof

set x = 1 / 2;
set y = 0 ;
reconsider x = 1 / 2, y = 0 as Element of [.0,1.] by XXREAL_1:1;
take x ; :: thesis: not for y being Element of [.0,1.] holds
( I_WB . (x,y) = 1 iff x <= y )
take y ; :: thesis: ( ( I_WB . (x,y) = 1 & not x <= y ) or ( x <= y & not I_WB . (x,y) = 1 ) )
thus ( ( I_WB . (x,y) = 1 & not x <= y ) or ( x <= y & not I_WB . (x,y) = 1 ) ) by FUZIMPL1:def 22; :: thesis: verum

end;

hence ( I_WB is satisfying_(NP) & I_WB is satisfying_(EP) & I_WB is satisfying_(IP) & not I_WB is satisfying_(OP) ) by CA, a0, BB, FUZIMPL1:def 22; :: thesis: verum