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