let AFV be WeakAffVect; :: thesis: for a, b, c, b9 being Element of AFV st Mid a,b,c & Mid a,b9,c & not b = b9 holds
MDist b,b9
let a, b, c, b9 be Element of AFV; :: thesis: ( Mid a,b,c & Mid a,b9,c & not b = b9 implies MDist b,b9 )
assume that
A1: Mid a,b,c and
A2: Mid a,b9,c ; :: thesis: ( b = b9 or MDist b,b9 )
A3: a,b // b,c by A1;
consider d being Element of AFV such that
A4: b9,c // b,d by Def1;
A5: b,d // b9,c by A4, Th3;
then b,b9 // d,c by Def1;
then A6: b9,b // c,d by Th7;
a,b9 // b9,c by A2;
then a,b9 // b,d by A5, Def1;
then b,b9 // c,d by A3, Def1;
then b,b9 // b9,b by A6, Def1;
hence ( b = b9 or MDist b,b9 ) ; :: thesis: verum