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