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 consider p, p' being Element of AFV such that
A1: p <> p' and
A2: a,b // p,p' and
a,p // p,b and
a,p' // p',b by Def4;
thus a <> b by A1, A2, Th2, Th6; :: thesis: verum