let AFV be WeakAffVect; :: thesis: ex a, b being Element of AFV st
( a <> b & not MDist a,b )
consider p, q being Element of AFV such that
A1: p <> q by STRUCT_0:def 10;

now

consider r being Element of AFV such that
A2: p,r // r,q by Def1;

A3: now

assume A4: p = r ; :: thesis: ex a, b being Element of AFV st
( a <> b & not MDist a,b )
then r,q // p,p by A2, Th4;
hence ex a, b being Element of AFV st
( a <> b & not MDist a,b ) by A1, A4, Def1; :: thesis: verum

end;

now

assume A5: p <> r ; :: thesis: ex a, b being Element of AFV st
( a <> b & not MDist a,b )

now

assume A6: MDist p,r ; :: thesis: ex a, b being Element of AFV st
( a <> b & not MDist a,b )
r,q // p,r by A2, Th4;
then A7: q,r // r,p by Th8;
p,r // r,p by A6, Def2;
then p,r // q,r by A7, Def1;
hence ex a, b being Element of AFV st
( a <> b & not MDist a,b ) by A1, Th5, Th8; :: thesis: verum

end;

hence ex a, b being Element of AFV st
( a <> b & not MDist a,b ) by A5; :: thesis: verum

end;

hence ex a, b being Element of AFV st
( a <> b & not MDist a,b ) by A3; :: thesis: verum

end;

hence ex a, b being Element of AFV st
( a <> b & not MDist a,b ) ; :: thesis: verum