theorem Th37: :: ORDERS_2:37

for A being non empty Poset
for f being Choice_Function of (BOOL the carrier of A)
for fC being Chain of f holds f . the carrier of A in fC