let AFV be WeakAffVect; for a, b being Element of AFV holds
( a = b or ex c being Element of AFV st
( ( a <> c & a,b '||' b,c ) or ex p, p9 being Element of AFV st
( p <> p9 & a,b '||' p,p9 & a,p '||' p,b & a,p9 '||' p9,b ) ) )
let a, b be Element of AFV; ( a = b or ex c being Element of AFV st
( ( a <> c & a,b '||' b,c ) or ex p, p9 being Element of AFV st
( p <> p9 & a,b '||' p,p9 & a,p '||' p,b & a,p9 '||' p9,b ) ) )
consider c being Element of AFV such that
A1:
a,b // b,c
by AFVECT0:def 1;
A2:
now ( not a = c or a = b or ex p, p9 being Element of AFV st
( p <> p9 & a,b '||' p,p9 & a,p '||' p,b & a,p9 '||' p9,b ) )assume
a = c
;
( a = b or ex p, p9 being Element of AFV st
( p <> p9 & a,b '||' p,p9 & a,p '||' p,b & a,p9 '||' p9,b ) )then consider p,
p9 being
Element of
AFV such that A3:
a,
b '||' p,
p9
and A4:
(
a,
p '||' p,
b &
a,
p9 '||' p9,
b )
by A1, Lm2;
(
p = p9 implies
a = b )
by A3, Lm5;
hence
(
a = b or ex
p,
p9 being
Element of
AFV st
(
p <> p9 &
a,
b '||' p,
p9 &
a,
p '||' p,
b &
a,
p9 '||' p9,
b ) )
by A3, A4;
verum end;
hence
( a = b or ex c being Element of AFV st
( ( a <> c & a,b '||' b,c ) or ex p, p9 being Element of AFV st
( p <> p9 & a,b '||' p,p9 & a,p '||' p,b & a,p9 '||' p9,b ) ) )
by A2; verum