let x, y be Element of [.0,1.]; ( ( 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 )
( x > 0 implies I_GG . (x,y) = min (1,(y / x)) )
assume S0:
x > 0
; I_GG . (x,y) = min (1,(y / x))
A1:
y >= 0
by XXREAL_1:1;