theorem Th23: :: ORDERS_2:23

for A being non empty Poset
for a, c being Element of A holds
( a < c iff a in LowerCone {c} )