set I = I_GD ;
A1: I_GD is satisfying_(OP)
proof
let x, y be Element of [.0,1.]; :: according to FUZIMPL2:def 4 :: thesis: ( I_GD . (x,y) = 1 iff x <= y )
( I_GD . (x,y) = 1 implies x <= y )
proof
assume T2: I_GD . (x,y) = 1 ; :: thesis: x <= y
assume T3: x > y ; :: thesis: contradiction
then I_GD . (x,y) = y by FUZIMPL1:def 16;
hence contradiction by T3, XXREAL_1:1, T2; :: thesis: verum
end;
hence ( I_GD . (x,y) = 1 iff x <= y ) by FUZIMPL1:def 16; :: thesis: verum
end;
for x, y, z being Element of [.0,1.] holds I_GD . (x,(I_GD . (y,z))) = I_GD . (y,(I_GD . (x,z)))
proof
let x, y, z be Element of [.0,1.]; :: thesis: I_GD . (x,(I_GD . (y,z))) = I_GD . (y,(I_GD . (x,z)))
AA: 1 in [.0,1.] by XXREAL_1:1;
per cases ( ( y <= z & x <= z ) or ( y > z & x <= z ) or ( y > z & x > z ) or ( y <= z & x > z ) ) ;
suppose YY: ( y <= z & x <= z ) ; :: thesis: I_GD . (x,(I_GD . (y,z))) = I_GD . (y,(I_GD . (x,z)))
then Y1: I_GD . (x,(I_GD . (y,z))) = I_GD . (x,1) by FUZIMPL1:def 16
.= 1 by FUZIMPL1:def 16, AA ;
I_GD . (y,(I_GD . (x,z))) = I_GD . (y,1) by YY, FUZIMPL1:def 16
.= 1 by AA, FUZIMPL1:def 16 ;
hence I_GD . (x,(I_GD . (y,z))) = I_GD . (y,(I_GD . (x,z))) by Y1; :: thesis: verum
end;
suppose YY: ( y > z & x <= z ) ; :: thesis: I_GD . (x,(I_GD . (y,z))) = I_GD . (y,(I_GD . (x,z)))
then Y1: I_GD . (x,(I_GD . (y,z))) = I_GD . (x,z) by FUZIMPL1:def 16
.= 1 by FUZIMPL1:def 16, YY ;
I_GD . (y,(I_GD . (x,z))) = I_GD . (y,1) by YY, FUZIMPL1:def 16
.= 1 by AA, FUZIMPL1:def 16 ;
hence I_GD . (x,(I_GD . (y,z))) = I_GD . (y,(I_GD . (x,z))) by Y1; :: thesis: verum
end;
suppose YY: ( y > z & x > z ) ; :: thesis: I_GD . (x,(I_GD . (y,z))) = I_GD . (y,(I_GD . (x,z)))
then Y1: I_GD . (x,(I_GD . (y,z))) = I_GD . (x,z) by FUZIMPL1:def 16
.= z by FUZIMPL1:def 16, YY ;
I_GD . (y,(I_GD . (x,z))) = I_GD . (y,z) by YY, FUZIMPL1:def 16
.= z by YY, FUZIMPL1:def 16 ;
hence I_GD . (x,(I_GD . (y,z))) = I_GD . (y,(I_GD . (x,z))) by Y1; :: thesis: verum
end;
suppose YY: ( y <= z & x > z ) ; :: thesis: I_GD . (x,(I_GD . (y,z))) = I_GD . (y,(I_GD . (x,z)))
then Y1: I_GD . (x,(I_GD . (y,z))) = I_GD . (x,1) by FUZIMPL1:def 16
.= 1 by FUZIMPL1:def 16, AA ;
I_GD . (y,(I_GD . (x,z))) = I_GD . (y,z) by YY, FUZIMPL1:def 16
.= 1 by YY, FUZIMPL1:def 16 ;
hence I_GD . (x,(I_GD . (y,z))) = I_GD . (y,(I_GD . (x,z))) by Y1; :: thesis: verum
end;
end;
end;
then I_GD is satisfying_(EP) ;
hence ( I_GD is satisfying_(NP) & I_GD is satisfying_(EP) & I_GD is satisfying_(IP) & I_GD is satisfying_(OP) ) by A1; :: thesis: verum