let AFV be WeakAffVect; :: thesis: for a, b being Element of AFV holds
( a,b // b,a iff ex p, q being Element of AFV st
( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b ) )
let a, b be Element of AFV; :: thesis: ( a,b // b,a iff ex p, q being Element of AFV st
( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b ) )

A1: now

assume A2: a,b // b,a ; :: thesis: ex p, q being Element of AFV st
( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b )

A3: now

assume A4: a = b ; :: thesis: ex p, q being Element of AFV st
( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b )
take p = a; :: thesis: ex q being Element of AFV st
( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b )
take q = a; :: thesis: ( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b )
( a,b // p,q & a,p // p,b & a,q // q,b ) by A4, AFVECT0:3;
hence ( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b ) by DIRAF:def 4; :: thesis: verum

end;

now

assume A5: a <> b ; :: thesis: ex p, q being Element of AFV st
( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b )
consider p being Element of AFV such that
A6: Mid a,p,b by AFVECT0:24;
consider q being Element of AFV such that
A7: a,b // p,q by AFVECT0:def 1;
MDist a,b by A2, A5, AFVECT0:def 2;
then A8: Mid a,q,b by A6, A7, AFVECT0:19, AFVECT0:28;
A9: a,p // p,b by A6, AFVECT0:def 3;
A10: a,q // q,b by A8, AFVECT0:def 3;
take p = p; :: thesis: ex q being Element of AFV st
( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b )
take q = q; :: thesis: ( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b )
thus ( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b ) by A7, A9, A10, DIRAF:def 4; :: thesis: verum

end;

hence ex p, q being Element of AFV st
( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b ) by A3; :: thesis: verum

end;

now

given p, q being Element of AFV such that A11: ( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b ) ; :: thesis: a,b // b,a

now

assume A12: a <> b ; :: thesis: a,b // b,a
then ( a,p // p,b & a,q // q,b ) by A11, Lm1;
then A13: ( Mid a,p,b & Mid a,q,b ) by AFVECT0:def 3;

A14: now

assume p = q ; :: thesis: contradiction
then a,b // p,p by A11, DIRAF:def 4;
hence contradiction by A12, AFVECT0:def 1; :: thesis: verum

end;

now

assume A15: MDist p,q ; :: thesis: a,b // b,a
( a,b // p,q or a,b // q,p ) by A11, DIRAF:def 4;
then MDist a,b by A15, AFVECT0:4, AFVECT0:19;
hence a,b // b,a by AFVECT0:def 2; :: thesis: verum

end;

hence a,b // b,a by A13, A14, AFVECT0:25; :: thesis: verum

end;

hence a,b // b,a by AFVECT0:3; :: thesis: verum

end;

hence ( a,b // b,a iff ex p, q being Element of AFV st
( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b ) ) by A1; :: thesis: verum