let AFV be WeakAffVect; :: thesis: for a, p, a9, b, q, b9 being Element of AFV st Mid a,p,a9 & Mid b,q,b9 & MDist p,q holds
a,b // b9,a9
let a, p, a9, b, q, b9 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, Th28;
hence a,b // b9,a9 by A2, Th30; :: thesis: verum