let AFV be WeakAffVect; :: thesis: for a, b, c, b' being Element of AFV st Mid a,b,c & Mid a,b',c & not b = b' holds
MDist b,b'
let a, b, c, b' be Element of AFV; :: thesis: ( Mid a,b,c & Mid a,b',c & not b = b' implies MDist b,b' )
assume ( Mid a,b,c & Mid a,b',c ) ; :: thesis: ( b = b' or MDist b,b' )
then A1: ( a,b // b,c & a,b' // b',c ) by Def3;
consider d being Element of AFV such that
A2: b',c // b,d by Def1;
A3: b,d // b',c by A2, Th4;
then a,b' // b,d by A1, Def1;
then A4: b,b' // c,d by A1, Def1;
b,b' // d,c by A3, Def1;
then b',b // c,d by Th8;
then b,b' // b',b by A4, Def1;
hence ( b = b' or MDist b,b' ) by Def2; :: thesis: verum