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