:: deftheorem Def1 defines greater_or_equal_to_id WAYBEL28:def 1 :
for N being non empty RelStr
for f being Function of N,N holds
( f is greater_or_equal_to_id iff for j being Element of N holds j <= f . j );