let AFV be WeakAffSegm; :: thesis: for a, b being Element of AFV st MDist a,b holds
a <> b
let a, b be Element of AFV; :: thesis: ( MDist a,b implies a <> b )
assume MDist a,b ; :: thesis: a <> b
then ex p, p9 being Element of AFV st
( p <> p9 & a,b // p,p9 & a,p // p,b & a,p9 // p9,b ) by Def4;
hence a <> b by Th2, Th6; :: thesis: verum