let AFV be WeakAffVect; 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; ( 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 )
; a,b9 '||' b9,c
A3:
b,b9 // b9,b
by A2, Lm2;
A4:
now ( a,b // b,c implies a,b9 '||' b9,c )assume A5:
a,
b // b,
c
;
a,b9 '||' b9,cthen A6:
Mid a,
b,
c
by AFVECT0:def 3;
A7:
now ( MDist b,b9 implies a,b9 '||' b9,c )assume
MDist b,
b9
;
a,b9 '||' b9,cthen
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;
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;
verum end;
now ( a,b // c,b implies a,b9 '||' b9,c )end;
hence
a,b9 '||' b9,c
by A1, A4, DIRAF:def 4; verum