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

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;

A2: now

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

end;

now

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;

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