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