:: deftheorem defines IntRel WAYBEL_4:def 2 :
for L being RelStr holds IntRel L = the InternalRel of L;