:: deftheorem defines SomePoints HILBERT4:def 3 :
for f being Function holds SomePoints f = (field f) \ (rng (ChoiceOn (FieldCover f)));