:: deftheorem Def2 defines with_comparable_down TAXONOM2:def 2 :
for A being RelStr holds
( A is with_comparable_down iff for x, y being Element of A holds
( for z being Element of A holds
( not z <= x or not z <= y ) or x <= y or y <= x ) );