:: deftheorem Def5 defines auxiliary(iii) WAYBEL_4:def 5 :
for L being non empty RelStr
for R being Relation of L holds
( R is auxiliary(iii) iff for x, y, z being Element of L st [x,z] in R & [y,z] in R holds
[(x "\/" y),z] in R );