for D being non empty set
for p, q being XFinSequence of D st p c= q holds
ex r being XFinSequence of D st p ^ r = q