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