let AFV be WeakAffVect; :: thesis: for a, b, c, c9 being Element of AFV st Mid a,b,c & Mid a,b,c9 holds
c = c9
let a, b, c, c9 be Element of AFV; :: thesis: ( Mid a,b,c & Mid a,b,c9 implies c = c9 )
assume that
A1: Mid a,b,c and
A2: Mid a,b,c9 ; :: thesis: c = c9
a,b // b,c9 by A2, Def3;
then A3: b,c9 // a,b by Th4;
a,b // b,c by A1, Def3;
then b,c // a,b by Th4;
then b,c // b,c9 by A3, Def1;
hence c = c9 by Th5; :: thesis: verum