:: deftheorem defines \ AOFA_I00:def 1 :
for F being non empty functional set
for x, f being set holds F \ (x,f) = { g where g is Element of F : g . x <> f } ;