let OAS be OAffinSpace; :: thesis: for a, a9, b, b9, p being Element of OAS st not p,a,a9 are_collinear & p,a // p,b & p,a9 // p,b9 & a,a9 '||' b,b9 holds
a,a9 // b,b9
let a, a9, b, b9, p be Element of OAS; :: thesis: ( not p,a,a9 are_collinear & p,a // p,b & p,a9 // p,b9 & a,a9 '||' b,b9 implies a,a9 // b,b9 )
assume that
A1: not p,a,a9 are_collinear and
A2: p,a // p,b and
A3: p,a9 // p,b9 and
A4: a,a9 '||' b,b9 ; :: thesis: a,a9 // b,b9
consider c being Element of OAS such that
A5: Mid a,p,c and
A6: p <> c by DIRAF:13;
A7: a,p // p,c by A5, DIRAF:def 3;
A8: a <> p by A1, DIRAF:31;
then consider c9 being Element of OAS such that
A9: a9,p // p,c9 and
A10: a9,a // c,c9 by A7, ANALOAF:def 5;
A11: a9,a '||' c9,c by A10, DIRAF:def 4;
A12: c <> c9

proof

assume c = c9 ; :: thesis: contradiction
then Mid a9,p,c by A9, DIRAF:def 3;
then a9,p,c are_collinear by DIRAF:28;
then A13: p,c,a9 are_collinear by DIRAF:30;
a,p,c are_collinear by A5, DIRAF:28;
then A14: p,c,a are_collinear by DIRAF:30;
p,c,p are_collinear by DIRAF:31;
hence contradiction by A1, A6, A14, A13, DIRAF:32; :: thesis: verum

end;

p,a // c,p by A7, DIRAF:2;
then c,p // p,b by A2, A8, ANALOAF:def 5;
then consider b99 being Element of OAS such that
A15: c9,p // p,b99 and
A16: c9,c // b,b99 by A6, ANALOAF:def 5;
A17: a9,a '||' b,b9 by A4, DIRAF:22;
A18: p <> c9

proof

assume p = c9 ; :: thesis: contradiction
then a9,a '||' c,p by A10, DIRAF:def 4;
then A19: p,c '||' a,a9 by DIRAF:22;
a,p '||' p,c by A7, DIRAF:def 4;
then a,p '||' a,a9 by A6, A19, DIRAF:23;
then a,p,a9 are_collinear by DIRAF:def 5;
hence contradiction by A1, DIRAF:30; :: thesis: verum

end;

p,a '||' p,b by A2, DIRAF:def 4;
then A20: p,a,b are_collinear by DIRAF:def 5;
A21: c9,c // a,a9 by A10, DIRAF:2;
a9,p '||' p,c9 by A9, DIRAF:def 4;
then A22: p,a9 '||' p,c9 by DIRAF:22;
p,a9 '||' p,b9 by A3, DIRAF:def 4;
then A23: p,a9,b9 are_collinear by DIRAF:def 5;
c9,p '||' p,b99 by A15, DIRAF:def 4;
then p,c9 '||' p,b99 by DIRAF:22;
then p,a9 '||' p,b99 by A18, A22, DIRAF:23;
then A24: p,a9,b99 are_collinear by DIRAF:def 5;
c9,c '||' b,b99 by A16, DIRAF:def 4;
then A25: a9,a '||' b,b99 by A12, A11, DIRAF:23;
not p,a9,a are_collinear by A1, DIRAF:30;
then c9,c // b,b9 by A20, A23, A17, A16, A24, A25, Th4;
hence a,a9 // b,b9 by A12, A21, ANALOAF:def 5; :: thesis: verum