let AFV be WeakAffSegm; :: thesis: for a, b, c being Element of AFV st MDist a,b & a,b // b,c holds
a = c
let a, b, c be Element of AFV; :: thesis: ( MDist a,b & a,b // b,c implies a = c )
assume that
A1: MDist a,b and
A2: a,b // b,c ; :: thesis: a = c
ex p, p9 being Element of AFV st
( p <> p9 & a,b // p,p9 & a,p // p,b & a,p9 // p9,b ) by A1, Def4;
hence a = c by A2, Th7; :: thesis: verum