:: deftheorem defines unordered LATTICEA:def 1 :
for IT being set holds
( IT is unordered iff for p1, p2 being set st p1 in IT & p2 in IT & p1 <> p2 holds
p1,p2 are_c=-incomparable );