for A being non empty Poset
for a, b being Element of A
for f being Choice_Function of (BOOL the carrier of A)
for fC being Chain of f st a in fC & b = f . the carrier of A holds
b <= a