let AFV be WeakAffVect; :: thesis: 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; :: thesis: ( 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 :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: verum
end;
now :: thesis: ( a <> c implies ex c being Element of AFV st
( a <> c & a,b '||' b,c ) )
assume A5: a <> c ; :: thesis: ex c being Element of AFV st
( a <> c & a,b '||' b,c )
a,b '||' b,c by A1, DIRAF:def 4;
hence ex c being Element of AFV st
( a <> c & a,b '||' b,c ) by A5; :: thesis: 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; :: thesis: verum