let AFV be WeakAffVect; :: thesis: for a, b being Element of holds
( a = b or ex c being Element of st
( ( a <> c & a,b '||' b,c ) or ex p, p' being Element of st
( p <> p' & a,b '||' p,p' & a,p '||' p,b & a,p' '||' p',b ) ) )
let a, b be Element of ; :: thesis: ( a = b or ex c being Element of st
( ( a <> c & a,b '||' b,c ) or ex p, p' being Element of st
( p <> p' & a,b '||' p,p' & a,p '||' p,b & a,p' '||' p',b ) ) )
consider c being Element of such that
A1: a,b // b,c by AFVECT0:def 1;

A2: now

assume a = c ; :: thesis: ( a = b or ex p, p' being Element of st
( p <> p' & a,b '||' p,p' & a,p '||' p,b & a,p' '||' p',b ) )
then consider p, p' being Element of such that
A3: a,b '||' p,p' and
A4: ( a,p '||' p,b & a,p' '||' p',b ) by A1, Lm2;
( p = p' implies a = b ) by A3, Lm5;
hence ( a = b or ex p, p' being Element of st
( p <> p' & a,b '||' p,p' & a,p '||' p,b & a,p' '||' p',b ) ) by A3, A4; :: thesis: verum

end;

now

assume A5: a <> c ; :: thesis: ex c being Element of st
( a <> c & a,b '||' b,c )
a,b '||' b,c by A1, DIRAF:def 4;
hence ex c being Element of st
( a <> c & a,b '||' b,c ) by A5; :: thesis: verum

end;

hence ( a = b or ex c being Element of st
( ( a <> c & a,b '||' b,c ) or ex p, p' being Element of st
( p <> p' & a,b '||' p,p' & a,p '||' p,b & a,p' '||' p',b ) ) ) by A2; :: thesis: verum