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