:: deftheorem Def6 defines auxiliary(iv) WAYBEL_4:def 6 :
for L being non empty RelStr
for R being Relation of L holds
( R is auxiliary(iv) iff for x being Element of L holds [(Bottom L),x] in R );