let AFV be WeakAffSegm; :: thesis: for a, b, c being Element of st MDist a,b & a,b // b,c holds
a = c
let a, b, c be Element of ; :: 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, p' being Element of st
( p <> p' & a,b // p,p' & a,p // p,b & a,p' // p',b ) by A1, Def4;
hence a = c by A2, Th7; :: thesis: verum