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