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