let AFV be WeakAffVect; :: thesis: for a, b, c, d being Element of AFV st MDist a,b & a,b // c,d holds
MDist c,d
let a, b, c, d be Element of AFV; :: thesis: ( MDist a,b & a,b // c,d implies MDist c,d )
assume that
A1: MDist a,b and
A2: a,b // c,d ; :: thesis: MDist c,d
A3: a,b // b,a by A1;
A4: c,d // a,b by A2, Th3;
then d,c // b,a by Th7;
then d,c // a,b by A3, Def1;
then c,d // d,c by A4, Def1;
then ( c <> d implies MDist c,d ) ;
hence MDist c,d by A1, A2, Def1; :: thesis: verum