:: deftheorem Def3 defines void YELLOW_3:def 3 :
for R being RelStr holds
( R is void iff the InternalRel of R is empty );