let AFV be WeakAffVect; 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 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 ( p <> r implies ex a, b being Element of AFV st
( a <> b & not MDist a,b ) )A4:
now ( MDist p,r implies ex a, b being Element of AFV st
( a <> b & not MDist a,b ) )assume
MDist p,
r
;
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;
verum end; assume
p <> r
;
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;
verum end; hence
ex
a,
b being
Element of
AFV st
(
a <> b & not
MDist a,
b )
by A3;
verum end;
hence
ex a, b being Element of AFV st
( a <> b & not MDist a,b )
; verum