:: deftheorem defines auxiliary WAYBEL_4:def 7 :
for L being non empty RelStr
for R being Relation of L holds
( R is auxiliary iff ( R is auxiliary(i) & R is auxiliary(ii) & R is auxiliary(iii) & R is auxiliary(iv) ) );