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