let AFV be WeakAffVect; :: thesis: for a, b, b9, p, p9, c being Element of AFV st a,b '||' b,c & b,b9 '||' p,p9 & b,p '||' p,b9 & b,p9 '||' p9,b9 holds
a,b9 '||' b9,c
let a, b, b9, p, p9, c be Element of AFV; :: thesis: ( a,b '||' b,c & b,b9 '||' p,p9 & b,p '||' p,b9 & b,p9 '||' p9,b9 implies a,b9 '||' b9,c )
assume that
A1: a,b '||' b,c and
A2: ( b,b9 '||' p,p9 & b,p '||' p,b9 & b,p9 '||' p9,b9 ) ; :: thesis: a,b9 '||' b9,c
A3: b,b9 // b9,b by A2, Lm2;
A4: now :: thesis: ( a,b // b,c implies a,b9 '||' b9,c )
assume A5: a,b // b,c ; :: thesis: a,b9 '||' b9,c
then A6: Mid a,b,c by AFVECT0:def 3;
A7: now :: thesis: ( MDist b,b9 implies a,b9 '||' b9,c )
assume MDist b,b9 ; :: thesis: a,b9 '||' b9,c
then Mid a,b9,c by A6, AFVECT0:23;
then a,b9 // b9,c by AFVECT0:def 3;
hence a,b9 '||' b9,c by DIRAF:def 4; :: thesis: verum
end;
( b = b9 implies a,b9 '||' b9,c ) by A5, DIRAF:def 4;
hence a,b9 '||' b9,c by A3, A7, AFVECT0:def 2; :: thesis: verum
end;
now :: thesis: ( a,b // c,b implies a,b9 '||' b9,c )
assume a,b // c,b ; :: thesis: a,b9 '||' b9,c
then a = c by AFVECT0:4, AFVECT0:7;
then a,b9 // c,b9 by AFVECT0:1;
hence a,b9 '||' b9,c by DIRAF:def 4; :: thesis: verum
end;
hence a,b9 '||' b9,c by A1, A4, DIRAF:def 4; :: thesis: verum