for x, y being Element of [.0,1.] holds
( ( x = 0 implies I_GG . (x,y) = 1 ) & ( x > 0 implies I_GG . (x,y) = min (1,(y / x)) ) )