theorem Th21: :: ORDERS_2:21

for A being non empty Poset
for a being Element of A holds not a in LowerCone {a}