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

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

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

end;

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

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

end;

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