theorem :: ORDERS_2:40

for A being non empty Poset
for f being Choice_Function of (BOOL the carrier of A)
for fC1, fC2 being Chain of f holds fC1 meets fC2