let AFV be WeakAffVect; :: thesis: for a, b, c, b9, c9 being Element of AFV st Mid a,b,c & Mid a,b9,c9 & MDist b,b9 holds
c = c9
let a, b, c, b9, c9 be Element of AFV; :: thesis: ( Mid a,b,c & Mid a,b9,c9 & MDist b,b9 implies c = c9 )
assume that
A1: Mid a,b,c and
A2: Mid a,b9,c9 and
A3: MDist b,b9 ; :: thesis: c = c9
Mid a,b9,c by A1, A3, Th23;
hence c = c9 by A2, Th22; :: thesis: verum