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