theorem Th45: :: ORDERS_2:45

for A being non empty Poset
for f being Choice_Function of (BOOL the carrier of A) holds union (Chains f) is Chain of f