for AFV being WeakAffSegm
for a, b being Element of AFV st MDist a,b holds
a <> b by Th2, Th6;