let x, y be Element of [.0,1.]; :: thesis: ( ( x = 0 implies I_GG . (x,y) = 1 ) & ( x > 0 implies I_GG . (x,y) = min (1,(y / x)) ) )
thus ( x = 0 implies I_GG . (x,y) = 1 ) :: thesis: ( x > 0 implies I_GG . (x,y) = min (1,(y / x)) )
proof
assume x = 0 ; :: thesis: I_GG . (x,y) = 1
then x <= y by XXREAL_1:1;
hence I_GG . (x,y) = 1 by FUZIMPL1:def 19; :: thesis: verum
end;
assume S0: x > 0 ; :: thesis: I_GG . (x,y) = min (1,(y / x))
A1: y >= 0 by XXREAL_1:1;
per cases ( x <= y or x > y ) ;
suppose A2: x <= y ; :: thesis: I_GG . (x,y) = min (1,(y / x))
then S1: I_GG . (x,y) = 1 by FUZIMPL1:def 19;
y / x >= 1 by A2, S0, XREAL_1:181;
hence I_GG . (x,y) = min (1,(y / x)) by S1, XXREAL_0:def 9; :: thesis: verum
end;
suppose S2: x > y ; :: thesis: I_GG . (x,y) = min (1,(y / x))
then I_GG . (x,y) = y / x by FUZIMPL1:def 19;
hence I_GG . (x,y) = min (1,(y / x)) by S2, A1, XREAL_1:183, XXREAL_0:def 9; :: thesis: verum
end;
end;