for AFV being WeakAffSegm
for a, b, c being Element of AFV st a,b // c,c holds
a = b