let AFV be WeakAffSegm; :: thesis: for a, b being Element of AFV st a <> b & not MDist a,b holds
ex c being Element of AFV st
( a <> c & a,b // b,c )
let a, b be Element of AFV; :: thesis: ( a <> b & not MDist a,b implies ex c being Element of AFV st
( a <> c & a,b // b,c ) )
assume A1: ( a <> b & not MDist a,b ) ; :: thesis: ex c being Element of AFV st
( a <> c & a,b // b,c )
( a = b or ex c being Element of AFV st
( ( a <> c & a,b // b,c ) or ex p, p9 being Element of AFV st
( p <> p9 & a,b // p,p9 & a,p // p,b & a,p9 // p9,b ) ) ) by Def2;
hence ex c being Element of AFV st
( a <> c & a,b // b,c ) by A1, Def4; :: thesis: verum