set I = I_GG ;

for x, y being Element of [.0,1.] holds

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

for x, y, z being Element of [.0,1.] holds I_GG . (x,(I_GG . (y,z))) = I_GG . (y,(I_GG . (x,z)))

hence ( I_GG is satisfying_(NP) & I_GG is satisfying_(EP) & I_GG is satisfying_(IP) & I_GG is satisfying_(OP) ) by A1; :: thesis: verum

for x, y being Element of [.0,1.] holds

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

proof

then A1:
I_GG is satisfying_(OP)
;
let x, y be Element of [.0,1.]; :: thesis: ( I_GG . (x,y) = 1 iff x <= y )

thus ( I_GG . (x,y) = 1 implies x <= y ) :: thesis: ( x <= y implies I_GG . (x,y) = 1 )

end;thus ( I_GG . (x,y) = 1 implies x <= y ) :: thesis: ( x <= y implies I_GG . (x,y) = 1 )

proof

thus
( x <= y implies I_GG . (x,y) = 1 )
by FUZIMPL1:def 19; :: thesis: verum
assume T2:
I_GG . (x,y) = 1
; :: thesis: x <= y

assume T3: x > y ; :: thesis: contradiction

then T4: x > 0 by XXREAL_1:1;

I_GG . (x,y) = y / x by T3, FUZIMPL1:def 19;

then y = 1 * x by XCMPLX_1:87, T4, T2;

hence contradiction by T3; :: thesis: verum

end;assume T3: x > y ; :: thesis: contradiction

then T4: x > 0 by XXREAL_1:1;

I_GG . (x,y) = y / x by T3, FUZIMPL1:def 19;

then y = 1 * x by XCMPLX_1:87, T4, T2;

hence contradiction by T3; :: thesis: verum

for x, y, z being Element of [.0,1.] holds I_GG . (x,(I_GG . (y,z))) = I_GG . (y,(I_GG . (x,z)))

proof

then
I_GG is satisfying_(EP)
;
let x, y, z be Element of [.0,1.]; :: thesis: I_GG . (x,(I_GG . (y,z))) = I_GG . (y,(I_GG . (x,z)))

AB: ( 0 <= x & x <= 1 ) by XXREAL_1:1;

AC: ( 0 <= y & y <= 1 ) by XXREAL_1:1;

AA: 1 in [.0,1.] by XXREAL_1:1;

end;AB: ( 0 <= x & x <= 1 ) by XXREAL_1:1;

AC: ( 0 <= y & y <= 1 ) by XXREAL_1:1;

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

end;

suppose YY:
( y <= z & x <= z )
; :: thesis: I_GG . (x,(I_GG . (y,z))) = I_GG . (y,(I_GG . (x,z)))

then Y1: I_GG . (x,(I_GG . (y,z))) =
I_GG . (x,1)
by FUZIMPL1:def 19

.= 1 by FUZIMPL1:def 19, AA, AB ;

I_GG . (y,(I_GG . (x,z))) = I_GG . (y,1) by YY, FUZIMPL1:def 19

.= 1 by AC, FUZIMPL1:def 19, AA ;

hence I_GG . (x,(I_GG . (y,z))) = I_GG . (y,(I_GG . (x,z))) by Y1; :: thesis: verum

end;.= 1 by FUZIMPL1:def 19, AA, AB ;

I_GG . (y,(I_GG . (x,z))) = I_GG . (y,1) by YY, FUZIMPL1:def 19

.= 1 by AC, FUZIMPL1:def 19, AA ;

hence I_GG . (x,(I_GG . (y,z))) = I_GG . (y,(I_GG . (x,z))) by Y1; :: thesis: verum

suppose YY:
( y > z & x <= z )
; :: thesis: I_GG . (x,(I_GG . (y,z))) = I_GG . (y,(I_GG . (x,z)))

x * y <= x
by XREAL_1:153, AC, AB;

then ( x * y <= z & y > 0 ) by YY, XXREAL_0:2;

then F1: x <= z / y by XREAL_1:77;

F2: z / y in [.0,1.] by YY, FUZIMPL1:6;

Y1: I_GG . (x,(I_GG . (y,z))) = I_GG . (x,(z / y)) by FUZIMPL1:def 19, YY

.= 1 by FUZIMPL1:def 19, F1, F2 ;

I_GG . (y,(I_GG . (x,z))) = I_GG . (y,1) by YY, FUZIMPL1:def 19

.= 1 by AC, AA, FUZIMPL1:def 19 ;

hence I_GG . (x,(I_GG . (y,z))) = I_GG . (y,(I_GG . (x,z))) by Y1; :: thesis: verum

end;then ( x * y <= z & y > 0 ) by YY, XXREAL_0:2;

then F1: x <= z / y by XREAL_1:77;

F2: z / y in [.0,1.] by YY, FUZIMPL1:6;

Y1: I_GG . (x,(I_GG . (y,z))) = I_GG . (x,(z / y)) by FUZIMPL1:def 19, YY

.= 1 by FUZIMPL1:def 19, F1, F2 ;

I_GG . (y,(I_GG . (x,z))) = I_GG . (y,1) by YY, FUZIMPL1:def 19

.= 1 by AC, AA, FUZIMPL1:def 19 ;

hence I_GG . (x,(I_GG . (y,z))) = I_GG . (y,(I_GG . (x,z))) by Y1; :: thesis: verum

suppose YY:
( y > z & x > z )
; :: thesis: I_GG . (x,(I_GG . (y,z))) = I_GG . (y,(I_GG . (x,z)))

then JJ:
( x > 0 & y > 0 )
by XXREAL_1:1;

end;per cases
( x <= z / y or x > z / y )
;

end;

suppose IK:
x <= z / y
; :: thesis: I_GG . (x,(I_GG . (y,z))) = I_GG . (y,(I_GG . (x,z)))

J1:
y > 0
by XXREAL_1:1, YY;

then x * y <= (z / y) * y by IK, XREAL_1:64;

then x * y <= z by J1, XCMPLX_1:87;

then (x * y) / x <= z / x by JJ, XREAL_1:72;

then FF: y <= z / x by JJ, XCMPLX_1:89;

F2: z / x in [.0,1.] by YY, FUZIMPL1:6;

F4: z / y in [.0,1.] by YY, FUZIMPL1:6;

Y1: I_GG . (x,(I_GG . (y,z))) = I_GG . (x,(z / y)) by FUZIMPL1:def 19, YY

.= 1 by FUZIMPL1:def 19, F4, IK ;

I_GG . (y,(I_GG . (x,z))) = I_GG . (y,(z / x)) by YY, FUZIMPL1:def 19

.= 1 by FUZIMPL1:def 19, F2, FF ;

hence I_GG . (x,(I_GG . (y,z))) = I_GG . (y,(I_GG . (x,z))) by Y1; :: thesis: verum

end;then x * y <= (z / y) * y by IK, XREAL_1:64;

then x * y <= z by J1, XCMPLX_1:87;

then (x * y) / x <= z / x by JJ, XREAL_1:72;

then FF: y <= z / x by JJ, XCMPLX_1:89;

F2: z / x in [.0,1.] by YY, FUZIMPL1:6;

F4: z / y in [.0,1.] by YY, FUZIMPL1:6;

Y1: I_GG . (x,(I_GG . (y,z))) = I_GG . (x,(z / y)) by FUZIMPL1:def 19, YY

.= 1 by FUZIMPL1:def 19, F4, IK ;

I_GG . (y,(I_GG . (x,z))) = I_GG . (y,(z / x)) by YY, FUZIMPL1:def 19

.= 1 by FUZIMPL1:def 19, F2, FF ;

hence I_GG . (x,(I_GG . (y,z))) = I_GG . (y,(I_GG . (x,z))) by Y1; :: thesis: verum

suppose F5:
x > z / y
; :: thesis: I_GG . (x,(I_GG . (y,z))) = I_GG . (y,(I_GG . (x,z)))

then
x * y > (z / y) * y
by JJ, XREAL_1:68;

then x * y > z by JJ, XCMPLX_1:87;

then (x * y) / x > z / x by XREAL_1:74, JJ;

then F1: y > z / x by XCMPLX_1:89, JJ;

F2: z / x in [.0,1.] by YY, FUZIMPL1:6;

F4: z / y in [.0,1.] by YY, FUZIMPL1:6;

Y1: I_GG . (x,(I_GG . (y,z))) = I_GG . (x,(z / y)) by FUZIMPL1:def 19, YY

.= (z / y) / x by FUZIMPL1:def 19, F5, F4 ;

I_GG . (y,(I_GG . (x,z))) = I_GG . (y,(z / x)) by YY, FUZIMPL1:def 19

.= (z / x) / y by FUZIMPL1:def 19, F2, F1 ;

hence I_GG . (x,(I_GG . (y,z))) = I_GG . (y,(I_GG . (x,z))) by Y1; :: thesis: verum

end;then x * y > z by JJ, XCMPLX_1:87;

then (x * y) / x > z / x by XREAL_1:74, JJ;

then F1: y > z / x by XCMPLX_1:89, JJ;

F2: z / x in [.0,1.] by YY, FUZIMPL1:6;

F4: z / y in [.0,1.] by YY, FUZIMPL1:6;

Y1: I_GG . (x,(I_GG . (y,z))) = I_GG . (x,(z / y)) by FUZIMPL1:def 19, YY

.= (z / y) / x by FUZIMPL1:def 19, F5, F4 ;

I_GG . (y,(I_GG . (x,z))) = I_GG . (y,(z / x)) by YY, FUZIMPL1:def 19

.= (z / x) / y by FUZIMPL1:def 19, F2, F1 ;

hence I_GG . (x,(I_GG . (y,z))) = I_GG . (y,(I_GG . (x,z))) by Y1; :: thesis: verum

suppose YY:
( y <= z & x > z )
; :: thesis: I_GG . (x,(I_GG . (y,z))) = I_GG . (y,(I_GG . (x,z)))

then F2:
z / x in [.0,1.]
by FUZIMPL1:6;

x * y <= y by XREAL_1:153, AC, AB;

then ( x * y <= z & x > 0 ) by YY, XXREAL_0:2;

then F1: y <= z / x by XREAL_1:77;

Y1: I_GG . (x,(I_GG . (y,z))) = I_GG . (x,1) by FUZIMPL1:def 19, YY

.= 1 by FUZIMPL1:def 19, AA, AB ;

I_GG . (y,(I_GG . (x,z))) = I_GG . (y,(z / x)) by YY, FUZIMPL1:def 19

.= 1 by FUZIMPL1:def 19, F2, F1 ;

hence I_GG . (x,(I_GG . (y,z))) = I_GG . (y,(I_GG . (x,z))) by Y1; :: thesis: verum

end;x * y <= y by XREAL_1:153, AC, AB;

then ( x * y <= z & x > 0 ) by YY, XXREAL_0:2;

then F1: y <= z / x by XREAL_1:77;

Y1: I_GG . (x,(I_GG . (y,z))) = I_GG . (x,1) by FUZIMPL1:def 19, YY

.= 1 by FUZIMPL1:def 19, AA, AB ;

I_GG . (y,(I_GG . (x,z))) = I_GG . (y,(z / x)) by YY, FUZIMPL1:def 19

.= 1 by FUZIMPL1:def 19, F2, F1 ;

hence I_GG . (x,(I_GG . (y,z))) = I_GG . (y,(I_GG . (x,z))) by Y1; :: thesis: verum

hence ( I_GG is satisfying_(NP) & I_GG is satisfying_(EP) & I_GG is satisfying_(IP) & I_GG is satisfying_(OP) ) by A1; :: thesis: verum