let AFV be WeakAffVect; for a, p, a', b, q, b' being Element of 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 ; ( Mid a,p,a' & Mid b,q,b' & MDist p,q implies a,b // b',a' )
assume that
A1:
Mid a,p,a'
and
A2:
Mid b,q,b'
and
A3:
MDist p,q
; a,b // b',a'
Mid a,q,a'
by A1, A3, Th28;
hence
a,b // b',a'
by A2, Th30; verum