let AFV be WeakAffVect; :: thesis: for a, b, c, b' being Element of st Mid a,b,c & Mid a,b',c & not b = b' holds
MDist b,b'
let a, b, c, b' be Element of ; :: thesis: ( Mid a,b,c & Mid a,b',c & not b = b' implies MDist b,b' )
assume that
A1: Mid a,b,c and
A2: Mid a,b',c ; :: thesis: ( b = b' or MDist b,b' )
A3: a,b // b,c by A1, Def3;
consider d being Element of such that
A4: b',c // b,d by Def1;
A5: b,d // b',c by A4, Th4;
then b,b' // d,c by Def1;
then A6: b',b // c,d by Th8;
a,b' // b',c by A2, Def3;
then a,b' // b,d by A5, Def1;
then b,b' // c,d by A3, Def1;
then b,b' // b',b by A6, Def1;
hence ( b = b' or MDist b,b' ) by Def2; :: thesis: verum