theorem :: ORDERS_2:16

for A being non empty Poset holds LowerCone ({} A) = the carrier of A