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