let AFV be WeakAffVect; for a, b being Element of AFV ex c being Element of AFV st Mid a,b,c
let a, b be Element of AFV; ex c being Element of AFV st Mid a,b,c
consider c being Element of AFV such that
A1:
a,b // b,c
by Def1;
Mid a,b,c
by A1;
hence
ex c being Element of AFV st Mid a,b,c
; verum