let AFV be WeakAffVect; 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; ( 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
; 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; verum