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 that
A1: Mid a,b,c and
A2: Mid a,b,c' ; :: thesis: c = c'
a,b // b,c' by A2, Def3;
then A3: b,c' // a,b by Th4;
a,b // b,c by A1, Def3;
then b,c // a,b by Th4;
then b,c // b,c' by A3, Def1;
hence c = c' by Th5; :: thesis: verum