let AFV be WeakAffVect; 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; ( 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
; a,b // b9,a9
Mid a,q,a9
by A1, A3, Th23;
hence
a,b // b9,a9
by A2, Th25; verum