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