let OAS be OAffinSpace; :: thesis: for p, a, b, p9, a9, b9 being Element of OAS st Mid p,a,b & p,a // p9,a9 & not LIN p,a,p9 & LIN p9,a9,b9 & p,p9 // a,a9 & p,p9 // b,b9 holds
Mid p9,a9,b9
let p, a, b, p9, a9, b9 be Element of OAS; :: thesis: ( Mid p,a,b & p,a // p9,a9 & not LIN p,a,p9 & LIN p9,a9,b9 & 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 LIN p,a,p9 and
A4: LIN p9,a9,b9 and
A5: p,p9 // a,a9 and
A6: p,p9 // b,b9 ; :: thesis: Mid p9,a9,b9
A7: p <> a by A3, DIRAF:37;
A8: p <> p9 by A3, DIRAF:37;
A9: LIN p,a,b by A1, DIRAF:34;
then A10: LIN p,b,a by DIRAF:36;

now

A11: p <> b by A1, A7, DIRAF:12;
A12: p9 <> b9

proof

assume A13: p9 = b9 ; :: thesis: contradiction
then b9,p // b9,b by A6, DIRAF:5;
then ( Mid b9,p,b or Mid b9,b,p ) by DIRAF:11;
then ( LIN b9,p,b or LIN b9,b,p ) by DIRAF:34;
then A14: LIN p,b,b9 by DIRAF:36;
LIN p,b,p by DIRAF:37;
hence contradiction by A3, A10, A11, A13, A14, DIRAF:38; :: thesis: verum

end;

A15: not LIN p,a,a9

proof

assume A16: LIN p,a,a9 ; :: thesis: contradiction
p,a '||' a9,p9 by A2, DIRAF:def 4;
hence contradiction by A3, A7, A16, DIRAF:39; :: thesis: verum

end;

then A17: a <> a9 by DIRAF:37;

A18: now

a,a9 // p,p9 by A5, DIRAF:5;
then A19: a,a9 '||' p9,p by DIRAF:def 4;
assume LIN a,a9,p9 ; :: thesis: contradiction
then LIN a,a9,p by A17, A19, DIRAF:39;
hence contradiction by A15, DIRAF:36; :: 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, Th26;
Mid b9,x,p by A21, DIRAF:13;
then consider y being Element of OAS such that
A23: Mid b9,y,p9 and
A24: p,p9 // x,y by Th26;
LIN b9,y,p9 by A23, DIRAF:34;
then A25: LIN p9,b9,y by DIRAF:36;
A26: b <> b9

proof

assume b = b9 ; :: thesis: contradiction
then LIN a9,p9,b by A4, DIRAF:36;
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:5;
then ( p,a // a9,b or p,a // b,a9 ) by A2, A20, DIRAF:6;
then p,a '||' b,a9 by DIRAF:def 4;
hence contradiction by A1, A7, A15, DIRAF:34, DIRAF:39; :: thesis: verum

end;

A27: x <> a

proof

assume x = a ; :: thesis: contradiction
then A28: LIN p,a,b9 by A21, DIRAF:34;
LIN p,a,a by DIRAF:37;
then A29: LIN b,b9,a by A7, A9, A28, DIRAF:38;
LIN p,a,p by DIRAF:37;
then A30: LIN b,b9,p by A7, A9, A28, DIRAF:38;
b,b9 // p,p9 by A6, DIRAF:5;
then b,b9 '||' p,p9 by DIRAF:def 4;
then LIN b,b9,p9 by A26, A30, DIRAF:39;
hence contradiction by A3, A26, A29, A30, DIRAF:38; :: thesis: verum

end;

A31: LIN p9,b9,a9 by A4, DIRAF:36;
then A32: LIN y,a9,a9 by A12, A25, DIRAF:38;
A33: p,p9 // a,x by A6, A22, A26, DIRAF:6;
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:6;
then a,y // a,a9 by A5, A8, ANALOAF:def 5;
then a,y '||' a,a9 by DIRAF:def 4;
then LIN a,y,a9 by DIRAF:def 5;
then A34: LIN y,a9,a by DIRAF:36;
LIN p9,b9,p9 by DIRAF:37;
then LIN y,a9,p9 by A12, A25, A31, DIRAF:38;
then ( y = a9 or LIN a,a9,p9 ) by A34, A32, DIRAF:38;
hence Mid p9,a9,b9 by A23, A18, DIRAF:13; :: thesis: verum

end;

hence Mid p9,a9,b9 by DIRAF:14; :: thesis: verum