:: deftheorem Def2 defines IFLGT PRGCOR_2:def 2 :
for x being object
for y being set
for a, b, c being object holds
( ( x in y implies IFLGT (x,y,a,b,c) = a ) & ( x = y implies IFLGT (x,y,a,b,c) = b ) & ( not x in y & not x = y implies IFLGT (x,y,a,b,c) = c ) );