:: deftheorem Def3 defines auxiliary(i) WAYBEL_4:def 3 :
for L being RelStr
for R being Relation of L holds
( R is auxiliary(i) iff for x, y being Element of L st [x,y] in R holds
x <= y );