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 :: thesis: ex a, b being Element of AFV st
( a <> b & not MDist a,b )
consider r being Element of AFV such that
A2: p,r // r,q by Def1;
A3: now :: thesis: ( p <> r implies ex a, b being Element of AFV st
( a <> b & not MDist a,b ) )
A4: now :: thesis: ( MDist p,r implies ex a, b being Element of AFV st
( a <> b & not MDist a,b ) )
assume MDist p,r ; :: thesis: ex a, b being Element of AFV st
( a <> b & not MDist a,b )
then A5: p,r // r,p ;
r,q // p,r by A2, Th3;
then q,r // r,p by Th7;
then p,r // q,r by A5, Def1;
hence ex a, b being Element of AFV st
( a <> b & not MDist a,b ) by A1, Th4, Th7; :: thesis: verum
end;
assume p <> r ; :: thesis: ex a, b being Element of AFV st
( a <> b & not MDist a,b )
hence ex a, b being Element of AFV st
( a <> b & not MDist a,b ) by A4; :: thesis: verum
end;
now :: thesis: ( p = r implies ex a, b being Element of AFV st
( a <> b & not MDist a,b ) )
assume A6: p = r ; :: thesis: ex a, b being Element of AFV st
( a <> b & not MDist a,b )
then r,q // p,p by A2, Th3;
hence ex a, b being Element of AFV st
( a <> b & not MDist a,b ) by A1, A6, Def1; :: 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