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