for A being non empty Poset
for a being Element of A
for f being Choice_Function of (BOOL the carrier of A)
for fC being Chain of f st a = f . the carrier of A holds
InitSegm (fC,a) = {}