let OAS be OAffinSpace; :: thesis: for a, b, c, d, p being Element of OAS st not p,a,b are_collinear & p,b // p,c & b,a // c,d & p <> d holds
not Mid a,p,d
let a, b, c, d, p be Element of OAS; :: thesis: ( not p,a,b are_collinear & p,b // p,c & b,a // c,d & p <> d implies not Mid a,p,d )
assume that
A1: not p,a,b are_collinear and
A2: p,b // p,c and
A3: b,a // c,d and
A4: p <> d ; :: thesis: not Mid a,p,d
assume Mid a,p,d ; :: thesis: contradiction
then Mid d,p,a by DIRAF:9;
then A5: d,p // p,a by DIRAF:def 3;
then A6: p,d // a,p by DIRAF:2;
consider b9 being Element of OAS such that
A7: c,p // p,b9 and
A8: c,d // a,b9 by A4, A5, ANALOAF:def 5;
A9: p <> c
proof
assume p = c ; :: thesis: contradiction
then b,a // a,p by A3, A4, A6, DIRAF:3;
then Mid b,a,p by DIRAF:def 3;
hence contradiction by A1, DIRAF:9, DIRAF:28; :: thesis: verum
end;
A10: a <> b9
proof
assume A11: a = b9 ; :: thesis: contradiction
b,p // c,p by A2, DIRAF:2;
then b,p // p,a by A9, A7, A11, DIRAF:3;
then Mid b,p,a by DIRAF:def 3;
then b,p,a are_collinear by DIRAF:28;
hence contradiction by A1, DIRAF:30; :: thesis: verum
end;
p,c // b9,p by A7, DIRAF:2;
then p,b // b9,p by A2, A9, DIRAF:3;
then A12: b9,p // p,b by DIRAF:2;
A13: c <> d
proof
assume c = d ; :: thesis: contradiction
then p,b // a,p by A2, A4, A6, DIRAF:3;
then b,p // p,a by DIRAF:2;
then Mid b,p,a by DIRAF:def 3;
then b,p,a are_collinear by DIRAF:28;
hence contradiction by A1, DIRAF:30; :: thesis: verum
end;
p <> b9
proof
assume p = b9 ; :: thesis: contradiction
then b,a // a,p by A3, A13, A8, DIRAF:3;
then Mid b,a,p by DIRAF:def 3;
hence contradiction by A1, DIRAF:9, DIRAF:28; :: thesis: verum
end;
then consider b99 being Element of OAS such that
A14: a,p // p,b99 and
A15: a,b9 // b,b99 by A12, ANALOAF:def 5;
a <> p by A1, DIRAF:31;
then A16: a <> b99 by A14, ANALOAF:def 5;
b,a // a,b9 by A3, A13, A8, DIRAF:3;
then b,a // b,b99 by A15, A10, DIRAF:3;
then ( Mid b,a,b99 or Mid b,b99,a ) by DIRAF:7;
then ( b,a,b99 are_collinear or b,b99,a are_collinear ) by DIRAF:28;
then A17: a,b99,b are_collinear by DIRAF:30;
Mid a,p,b99 by A14, DIRAF:def 3;
then a,p,b99 are_collinear by DIRAF:28;
then A18: a,b99,p are_collinear by DIRAF:30;
a,b99,a are_collinear by DIRAF:31;
hence contradiction by A1, A18, A16, A17, DIRAF:32; :: thesis: verum