let AFV be WeakAffVect; :: thesis: for a, b being Element of AFV holds
( Mid a,b,a iff ( a = b or MDist a,b ) )
let a, b be Element of AFV; :: thesis: ( Mid a,b,a iff ( a = b or MDist a,b ) )

A1: now :: thesis: ( a = b implies Mid a,b,a )

assume a = b ; :: thesis: Mid a,b,a
then a,b // b,a by Th6;
hence Mid a,b,a by Def3; :: thesis: verum

end;

A2: now :: thesis: ( MDist a,b implies Mid a,b,a )

assume MDist a,b ; :: thesis: Mid a,b,a
then a,b // b,a by Def2;
hence Mid a,b,a by Def3; :: thesis: verum

end;

now :: thesis: ( not Mid a,b,a or a = b or MDist a,b )

assume Mid a,b,a ; :: thesis: ( a = b or MDist a,b )
then a,b // b,a by Def3;
hence ( a = b or MDist a,b ) by Def2; :: thesis: verum

end;

hence ( Mid a,b,a iff ( a = b or MDist a,b ) ) by A1, A2; :: thesis: verum