:: deftheorem defines hierarchic TAXONOM2:def 3 :
for Y being set holds
( Y is hierarchic iff for x, y being set st x in Y & y in Y & not x c= y & not y c= x holds
x misses y );