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