:: deftheorem Def10 defines IFGT XXREAL_0:def 11 :
for x, y being ExtReal
for a, b being object holds
( ( x > y implies IFGT (x,y,a,b) = a ) & ( not x > y implies IFGT (x,y,a,b) = b ) );