let OAS be OAffinSpace; :: thesis: for a, a9, b, b9, p, p9 being Element of OAS st Mid p,a,b & p,a // p9,a9 & not p,a,p9 are_collinear & p9,a9,b9 are_collinear & p,p9 // a,a9 & p,p9 // b,b9 holds
Mid p9,a9,b9
let a, a9, b, b9, p, p9 be Element of OAS; :: thesis: ( Mid p,a,b & p,a // p9,a9 & not p,a,p9 are_collinear & p9,a9,b9 are_collinear & p,p9 // a,a9 & p,p9 // b,b9 implies Mid p9,a9,b9 )
assume that
A1: Mid p,a,b and
A2: p,a // p9,a9 and
A3: not p,a,p9 are_collinear and
A4: p9,a9,b9 are_collinear and
A5: p,p9 // a,a9 and
A6: p,p9 // b,b9 ; :: thesis: Mid p9,a9,b9
A7: p <> a by A3, DIRAF:31;
A8: p <> p9 by A3, DIRAF:31;
A9: p,a,b are_collinear by A1, DIRAF:28;
then A10: p,b,a are_collinear by DIRAF:30;
now :: thesis: ( p9 <> a9 & a9 <> b9 implies Mid p9,a9,b9 )
A11: p <> b by A1, A7, DIRAF:8;
A12: p9 <> b9
proof
assume A13: p9 = b9 ; :: thesis: contradiction
then b9,p // b9,b by A6, DIRAF:2;
then ( Mid b9,p,b or Mid b9,b,p ) by DIRAF:7;
then ( b9,p,b are_collinear or b9,b,p are_collinear ) by DIRAF:28;
then A14: p,b,b9 are_collinear by DIRAF:30;
p,b,p are_collinear by DIRAF:31;
hence contradiction by A3, A10, A11, A13, A14, DIRAF:32; :: thesis: verum
end;
A15: not p,a,a9 are_collinear
proof
assume A16: p,a,a9 are_collinear ; :: thesis: contradiction
p,a '||' a9,p9 by A2, DIRAF:def 4;
hence contradiction by A3, A7, A16, DIRAF:33; :: thesis: verum
end;
then A17: a <> a9 by DIRAF:31;
A18: now :: thesis: not a,a9,p9 are_collinear
a,a9 // p,p9 by A5, DIRAF:2;
then A19: a,a9 '||' p9,p by DIRAF:def 4;
assume a,a9,p9 are_collinear ; :: thesis: contradiction
then a,a9,p are_collinear by A17, A19, DIRAF:33;
hence contradiction by A15, DIRAF:30; :: thesis: verum
end;
assume that
A20: p9 <> a9 and
a9 <> b9 ; :: thesis: Mid p9,a9,b9
consider x being Element of OAS such that
A21: Mid p,x,b9 and
A22: b,b9 // a,x by A1, Th19;
Mid b9,x,p by A21, DIRAF:9;
then consider y being Element of OAS such that
A23: Mid b9,y,p9 and
A24: p,p9 // x,y by Th19;
b9,y,p9 are_collinear by A23, DIRAF:28;
then A25: p9,b9,y are_collinear by DIRAF:30;
A26: b <> b9
proof
assume b = b9 ; :: thesis: contradiction
then a9,p9,b are_collinear by A4, DIRAF:30;
then a9,p9 '||' a9,b by DIRAF:def 5;
then ( a9,p9 // a9,b or a9,p9 // b,a9 ) by DIRAF:def 4;
then ( p9,a9 // a9,b or p9,a9 // b,a9 ) by DIRAF:2;
then ( p,a // a9,b or p,a // b,a9 ) by A2, A20, DIRAF:3;
then p,a '||' b,a9 by DIRAF:def 4;
hence contradiction by A1, A7, A15, DIRAF:28, DIRAF:33; :: thesis: verum
end;
A27: x <> a
proof
assume x = a ; :: thesis: contradiction
then A28: p,a,b9 are_collinear by A21, DIRAF:28;
p,a,a are_collinear by DIRAF:31;
then A29: b,b9,a are_collinear by A7, A9, A28, DIRAF:32;
p,a,p are_collinear by DIRAF:31;
then A30: b,b9,p are_collinear by A7, A9, A28, DIRAF:32;
b,b9 // p,p9 by A6, DIRAF:2;
then b,b9 '||' p,p9 by DIRAF:def 4;
then b,b9,p9 are_collinear by A26, A30, DIRAF:33;
hence contradiction by A3, A26, A29, A30, DIRAF:32; :: thesis: verum
end;
A31: p9,b9,a9 are_collinear by A4, DIRAF:30;
then A32: y,a9,a9 are_collinear by A12, A25, DIRAF:32;
A33: p,p9 // a,x by A6, A22, A26, DIRAF:3;
then a,x // x,y by A8, A24, ANALOAF:def 5;
then a,x // a,y by ANALOAF:def 5;
then p,p9 // a,y by A27, A33, DIRAF:3;
then a,y // a,a9 by A5, A8, ANALOAF:def 5;
then a,y '||' a,a9 by DIRAF:def 4;
then a,y,a9 are_collinear by DIRAF:def 5;
then A34: y,a9,a are_collinear by DIRAF:30;
p9,b9,p9 are_collinear by DIRAF:31;
then y,a9,p9 are_collinear by A12, A25, A31, DIRAF:32;
then ( y = a9 or a,a9,p9 are_collinear ) by A34, A32, DIRAF:32;
hence Mid p9,a9,b9 by A23, A18, DIRAF:9; :: thesis: verum
end;
hence Mid p9,a9,b9 by DIRAF:10; :: thesis: verum