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 ;
I_WB . (y,(I_WB . (x,z))) = I_WB . (y,z) by
.= z by ;
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 ;
hence I_WB . (x,(I_WB . (y,z))) = I_WB . (y,(I_WB . (x,z))) by ; :: 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 ;
hence I_WB . (x,(I_WB . (y,z))) = I_WB . (y,(I_WB . (x,z))) by ; :: 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 ; :: 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 ; :: thesis: verum