:: deftheorem Def1 defines IFIN MATRIX_7:def 1 :
for x being object
for y being set
for a, b being object holds
( ( x in y implies IFIN (x,y,a,b) = a ) & ( not x in y implies IFIN (x,y,a,b) = b ) );