set I = I_{1} ;
a2: for x being Element of [.0,1.] holds I_{1} . (x,x) = 1
proof
let x be Element of [.0,1.]; :: thesis: I_{1} . (x,x) = 1
( 0 <= x & x <= 1 ) by XXREAL_1:1;
per cases then ( x = 0 or ( 0 < x & x < 1 ) or x = 1 ) by XXREAL_0:1;
suppose ( 0 < x & x < 1 ) ; :: thesis: I_{1} . (x,x) = 1
hence I_{1} . (x,x) = 1 by FUZIMPL1:def 25; :: thesis: verum
end;
suppose x = 1 ; :: thesis: I_{1} . (x,x) = 1
hence I_{1} . (x,x) = 1 by FUZIMPL1:def 25; :: thesis: verum
end;
end;
end;
SS: 1 in [.0,1.] by XXREAL_1:1;
not for y being Element of [.0,1.] holds I_{1} . (1,y) = y
proof
reconsider y = 1 / 2 as Element of [.0,1.] by XXREAL_1:1;
I_{1} . (1,y) = 1 by ;
hence not for y being Element of [.0,1.] holds I_{1} . (1,y) = y ; :: thesis: verum
end;
then A3: not I_{1} is satisfying_(NP) ;
for x, y, z being Element of [.0,1.] holds I_{1} . (x,(I_{1} . (y,z))) = I_{1} . (y,(I_{1} . (x,z)))
proof
let x, y, z be Element of [.0,1.]; :: thesis: I_{1} . (x,(I_{1} . (y,z))) = I_{1} . (y,(I_{1} . (x,z)))
( y <= 1 & x <= 1 & z >= 0 ) by XXREAL_1:1;
per cases then ( ( z = 0 & x = 1 & y = 1 ) or ( z > 0 & x = 1 & y = 1 ) or ( z = 0 & x = 1 & y < 1 ) or ( z = 0 & x < 1 & y = 1 ) or ( z = 0 & x < 1 & y < 1 ) or ( z > 0 & x < 1 & y = 1 ) or ( z > 0 & x = 1 & y < 1 ) or ( z > 0 & x < 1 & y < 1 ) ) by XXREAL_0:1;
suppose B1: ( z = 0 & x = 1 & y = 1 ) ; :: thesis: I_{1} . (x,(I_{1} . (y,z))) = I_{1} . (y,(I_{1} . (x,z)))
then B2: I_{1} . (x,(I_{1} . (y,z))) = I_{1} . (x,0) by FUZIMPL1:def 25
.= 0 by ;
I_{1} . (y,(I_{1} . (x,z))) = I_{1} . (y,0) by
.= 0 by ;
hence I_{1} . (x,(I_{1} . (y,z))) = I_{1} . (y,(I_{1} . (x,z))) by B2; :: thesis: verum
end;
suppose B1: ( z > 0 & x = 1 & y = 1 ) ; :: thesis: I_{1} . (x,(I_{1} . (y,z))) = I_{1} . (y,(I_{1} . (x,z)))
then B2: I_{1} . (x,(I_{1} . (y,z))) = I_{1} . (x,1) by FUZIMPL1:def 25
.= 1 by ;
I_{1} . (y,(I_{1} . (x,z))) = I_{1} . (y,1) by
.= 1 by ;
hence I_{1} . (x,(I_{1} . (y,z))) = I_{1} . (y,(I_{1} . (x,z))) by B2; :: thesis: verum
end;
suppose B1: ( z = 0 & x = 1 & y < 1 ) ; :: thesis: I_{1} . (x,(I_{1} . (y,z))) = I_{1} . (y,(I_{1} . (x,z)))
then I_{1} . (x,(I_{1} . (y,z))) = I_{1} . (x,1) by FUZIMPL1:def 25
.= 1 by ;
hence I_{1} . (x,(I_{1} . (y,z))) = I_{1} . (y,(I_{1} . (x,z))) by ; :: thesis: verum
end;
suppose B1: ( z = 0 & x < 1 & y = 1 ) ; :: thesis: I_{1} . (x,(I_{1} . (y,z))) = I_{1} . (y,(I_{1} . (x,z)))
then I_{1} . (y,(I_{1} . (x,z))) = I_{1} . (y,1) by FUZIMPL1:def 25
.= 1 by ;
hence I_{1} . (x,(I_{1} . (y,z))) = I_{1} . (y,(I_{1} . (x,z))) by ; :: thesis: verum
end;
suppose B1: ( z = 0 & x < 1 & y < 1 ) ; :: thesis: I_{1} . (x,(I_{1} . (y,z))) = I_{1} . (y,(I_{1} . (x,z)))
then I_{1} . (y,(I_{1} . (x,z))) = 1 by FUZIMPL1:def 25;
hence I_{1} . (x,(I_{1} . (y,z))) = I_{1} . (y,(I_{1} . (x,z))) by ; :: thesis: verum
end;
suppose B1: ( z > 0 & x < 1 & y = 1 ) ; :: thesis: I_{1} . (x,(I_{1} . (y,z))) = I_{1} . (y,(I_{1} . (x,z)))
then I_{1} . (y,(I_{1} . (x,z))) = I_{1} . (y,1) by FUZIMPL1:def 25
.= 1 by ;
hence I_{1} . (x,(I_{1} . (y,z))) = I_{1} . (y,(I_{1} . (x,z))) by ; :: thesis: verum
end;
suppose B1: ( z > 0 & x = 1 & y < 1 ) ; :: thesis: I_{1} . (x,(I_{1} . (y,z))) = I_{1} . (y,(I_{1} . (x,z)))
then I_{1} . (x,(I_{1} . (y,z))) = I_{1} . (x,1) by FUZIMPL1:def 25
.= 1 by ;
hence I_{1} . (x,(I_{1} . (y,z))) = I_{1} . (y,(I_{1} . (x,z))) by ; :: thesis: verum
end;
suppose F1: ( z > 0 & x < 1 & y < 1 ) ; :: thesis: I_{1} . (x,(I_{1} . (y,z))) = I_{1} . (y,(I_{1} . (x,z)))
then I_{1} . (y,(I_{1} . (x,z))) = 1 by FUZIMPL1:def 25;
hence I_{1} . (x,(I_{1} . (y,z))) = I_{1} . (y,(I_{1} . (x,z))) by ; :: thesis: verum
end;
end;
end;
then I_{1} is satisfying_(EP) ;
hence ( not I_{1} is satisfying_(NP) & I_{1} is satisfying_(EP) & I_{1} is satisfying_(IP) & not I_{1} is satisfying_(OP) ) by a2, A3; :: thesis: verum