let AFV be WeakAffVect; :: thesis: for a, b, a9, b9, p, q being Element of AFV st Mid a,p,a9 & Mid b,q,b9 & MDist p,q holds
a,b // b9,a9
let a, b, a9, b9, p, q be Element of AFV; :: thesis: ( Mid a,p,a9 & Mid b,q,b9 & MDist p,q implies a,b // b9,a9 )
assume that
A1: Mid a,p,a9 and
A2: Mid b,q,b9 and
A3: MDist p,q ; :: thesis: a,b // b9,a9
Mid a,q,a9 by A1, A3, Th23;
hence a,b // b9,a9 by A2, Th25; :: thesis: verum