theorem Th55: :: ORDERS_2:55

for A being non empty Poset st ( for C being Chain of A ex a being Element of A st
for b being Element of A st b in C holds
b <= a ) holds
ex a being Element of A st
for b being Element of A holds not a < b