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