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

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

end;

now

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