let AFV be WeakAffVect; for a, b being Element of AFV holds
( a,b // b,a iff ex p, q being Element of AFV st
( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b ) )
let a, b be Element of AFV; ( a,b // b,a iff ex p, q being Element of AFV st
( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b ) )
A1:
now ( ex p, q being Element of AFV st
( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b ) implies a,b // b,a )given p,
q being
Element of
AFV such that A2:
a,
b '||' p,
q
and A3:
a,
p '||' p,
b
and A4:
a,
q '||' q,
b
;
a,b // b,anow ( a <> b implies a,b // b,a )A5:
now ( MDist p,q implies a,b // b,a )assume A6:
MDist p,
q
;
a,b // b,a
(
a,
b // p,
q or
a,
b // q,
p )
by A2, DIRAF:def 4;
then
MDist a,
b
by A6, AFVECT0:3, AFVECT0:15;
hence
a,
b // b,
a
by AFVECT0:def 2;
verum end; assume A7:
a <> b
;
a,b // b,athen
a,
q // q,
b
by A4, Lm1;
then A8:
Mid a,
q,
b
by AFVECT0:def 3;
a,
p // p,
b
by A3, A7, Lm1;
then
Mid a,
p,
b
by AFVECT0:def 3;
hence
a,
b // b,
a
by A8, A9, A5, AFVECT0:20;
verum end; hence
a,
b // b,
a
by AFVECT0:2;
verum end;
now ( a,b // b,a implies ex p, q being Element of AFV st
( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b ) )assume A10:
a,
b // b,
a
;
ex p, q being Element of AFV st
( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b )A11:
now ( a <> b implies ex p, q being Element of AFV st
( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b ) )assume
a <> b
;
ex p, q being Element of AFV st
( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b )then A12:
MDist a,
b
by A10, AFVECT0:def 2;
consider p being
Element of
AFV such that A13:
Mid a,
p,
b
by AFVECT0:19;
A14:
a,
p // p,
b
by A13, AFVECT0:def 3;
consider q being
Element of
AFV such that A15:
a,
b // p,
q
by AFVECT0:def 1;
take p =
p;
ex q being Element of AFV st
( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b )take q =
q;
( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b )
Mid a,
q,
b
by A13, A15, A12, AFVECT0:15, AFVECT0:23;
then
a,
q // q,
b
by AFVECT0:def 3;
hence
(
a,
b '||' p,
q &
a,
p '||' p,
b &
a,
q '||' q,
b )
by A15, A14, DIRAF:def 4;
verum end; now ( a = b implies ex p, q being Element of AFV st
( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b ) )assume A16:
a = b
;
ex p, q being Element of AFV st
( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b )take p =
a;
ex q being Element of AFV st
( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b )take q =
a;
( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b )
a,
b // p,
q
by A16, AFVECT0:2;
hence
(
a,
b '||' p,
q &
a,
p '||' p,
b &
a,
q '||' q,
b )
by A16, DIRAF:def 4;
verum end; hence
ex
p,
q being
Element of
AFV st
(
a,
b '||' p,
q &
a,
p '||' p,
b &
a,
q '||' q,
b )
by A11;
verum end;
hence
( a,b // b,a iff ex p, q being Element of AFV st
( a,b '||' p,q & a,p '||' p,b & a,q '||' q,b ) )
by A1; verum