let AFV be WeakAffVect; :: thesis: for a, p, a', b, q, b' being Element of AFV st Mid a,p,a' & Mid b,q,b' & MDist p,q holds
a,b // b',a'
let a, p, a', b, q, b' be Element of AFV; :: thesis: ( Mid a,p,a' & Mid b,q,b' & MDist p,q implies a,b // b',a' )
assume A1: ( Mid a,p,a' & Mid b,q,b' & MDist p,q ) ; :: thesis: a,b // b',a'
then Mid a,q,a' by Th28;
hence a,b // b',a' by A1, Th30; :: thesis: verum