:: deftheorem defines with_superior TAXONOM2:def 1 :
for A being RelStr holds
( A is with_superior iff ex x being Element of A st x is_superior_of the InternalRel of A );