:: deftheorem defines OtherPoints HILBERT4:def 4 :
for f being Function holds OtherPoints f = ((field f) \ (fixpoints f)) \ (SomePoints f);