set I = I_WB ;

a0: for x being Element of [.0,1.] holds I_WB . (x,x) = 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)))

( I_WB . (x,y) = 1 iff x <= y )

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

proof

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

x <= 1 by XXREAL_1:1;

end;x <= 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

not for x, y being Element of [.0,1.] holds
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;

end;( 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;

end;

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;.= 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

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;.= 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

( I_WB . (x,y) = 1 iff x <= y )

proof

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
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;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