let AFV be WeakAffVect; :: thesis: for a, b, c, b', c' being Element of AFV st Mid a,b,c & Mid a,b',c' & MDist b,b' holds
c = c'
let a, b, c, b', c' be Element of AFV; :: thesis: ( Mid a,b,c & Mid a,b',c' & MDist b,b' implies c = c' )
assume A1: ( Mid a,b,c & Mid a,b',c' & MDist b,b' ) ; :: thesis: c = c'
then Mid a,b',c by Th28;
hence c = c' by A1, Th27; :: thesis: verum