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