theorem Th36: :: ORDERS_2:36

for A being non empty Poset
for f being Choice_Function of (BOOL the carrier of A) holds {(f . the carrier of A)} is Chain of f