for A being non empty Poset
for S being Subset of A
for f being Choice_Function of (BOOL the carrier of A)
for fC being Chain of f st fC <> union (Chains f) & S = union (Chains f) holds
fC is Initial_Segm of S