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 that
A1: MDist a,b and
A2: MDist a,c ; :: thesis: ( b = c or MDist b,c )
A3: a,b // b,a by A1;
A4: a,c // c,a by A2;
consider d being Element of AFV such that
A5: c,a // b,d by Def1;
b,d // c,a by A5, Th3;
then a,c // b,d by A4, Def1;
then A6: b,c // a,d by A3, Def1;
c,b // a,d by A5, Def1;
then b,c // c,b by A6, Def1;
hence ( b = c or MDist b,c ) ; :: thesis: verum