let OAS be OAffinSpace; :: thesis: for p, a, b, p', a', b' being Element of OAS st Mid p,a,b & p,a // p',a' & not LIN p,a,p' & LIN p',a',b' & p,p' // a,a' & p,p' // b,b' holds
Mid p',a',b'
let p, a, b, p', a', b' be Element of OAS; :: thesis: ( Mid p,a,b & p,a // p',a' & not LIN p,a,p' & LIN p',a',b' & p,p' // a,a' & p,p' // b,b' implies Mid p',a',b' )
assume that
A1: Mid p,a,b and
A2: p,a // p',a' and
A3: not LIN p,a,p' and
A4: LIN p',a',b' and
A5: p,p' // a,a' and
A6: p,p' // b,b' ; :: thesis: Mid p',a',b'
A7: ( p <> a & p <> p' & a <> p' ) by A3, DIRAF:37;
A8: LIN p,a,b by A1, DIRAF:34;
then A9: LIN p,b,a by DIRAF:36;

now

assume A10: ( p' <> a' & a' <> b' ) ; :: thesis: Mid p',a',b'
consider x being Element of OAS such that
A11: Mid p,x,b' and
A12: b,b' // a,x by A1, Th26;
Mid b',x,p by A11, DIRAF:13;
then consider y being Element of OAS such that
A13: Mid b',y,p' and
A14: p,p' // x,y by Th26;
A15: ( LIN b',y,p' & LIN p,x,b' ) by A11, A13, DIRAF:34;
A16: not LIN p,a,a'

proof

assume LIN p,a,a' ; :: thesis: contradiction
then ( LIN p,a,a' & p,a '||' a',p' ) by A2, DIRAF:def 4;
hence contradiction by A3, A7, DIRAF:39; :: thesis: verum

end;

then A17: a <> a' by DIRAF:37;
A18: b <> b'

proof

assume b = b' ; :: thesis: contradiction
then LIN a',p',b by A4, DIRAF:36;
then a',p' '||' a',b by DIRAF:def 5;
then ( a',p' // a',b or a',p' // b,a' ) by DIRAF:def 4;
then ( p',a' // a',b or p',a' // b,a' ) by DIRAF:5;
then ( p,a // a',b or p,a // b,a' ) by A2, A10, DIRAF:6;
then p,a '||' b,a' by DIRAF:def 4;
hence contradiction by A1, A7, A16, DIRAF:34, DIRAF:39; :: thesis: verum

end;

A19: x <> a

proof

assume x = a ; :: thesis: contradiction
then ( LIN p,a,b' & LIN p,a,a & LIN p,a,p ) by A11, DIRAF:34, DIRAF:37;
then A20: ( LIN b,b',a & LIN b,b',p ) by A7, A8, DIRAF:38;
b,b' // p,p' by A6, DIRAF:5;
then b,b' '||' p,p' by DIRAF:def 4;
then LIN b,b',p' by A18, A20, DIRAF:39;
hence contradiction by A3, A18, A20, DIRAF:38; :: thesis: verum

end;

A21: p <> b by A1, A7, DIRAF:12;
A22: p' <> b'

proof

assume A23: p' = b' ; :: thesis: contradiction
then b',p // b',b by A6, DIRAF:5;
then ( Mid b',p,b or Mid b',b,p ) by DIRAF:11;
then ( LIN b',p,b or LIN b',b,p ) by DIRAF:34;
then ( LIN p,b,b' & LIN p,b,b & LIN p,b,p ) by DIRAF:36, DIRAF:37;
hence contradiction by A3, A9, A21, A23, DIRAF:38; :: thesis: verum

end;

A24: p,p' // a,x by A6, A12, A18, DIRAF:6;
then a,x // x,y by A7, A14, ANALOAF:def 5;
then a,x // a,y by ANALOAF:def 5;
then p,p' // a,y by A19, A24, DIRAF:6;
then a,y // a,a' by A5, A7, ANALOAF:def 5;
then a,y '||' a,a' by DIRAF:def 4;
then LIN a,y,a' by DIRAF:def 5;
then A25: LIN y,a',a by DIRAF:36;
( LIN p',b',y & LIN p',b',a' & LIN p',b',p' ) by A4, A15, DIRAF:36, DIRAF:37;
then ( LIN y,a',p' & LIN y,a',a' ) by A22, DIRAF:38;
then A26: ( y = a' or LIN a,a',p' ) by A25, DIRAF:38;

now

assume LIN a,a',p' ; :: thesis: contradiction
then ( LIN a,a',p' & a,a' // p,p' ) by A5, DIRAF:5;
then ( LIN a,a',p' & a,a' '||' p',p ) by DIRAF:def 4;
then LIN a,a',p by A17, DIRAF:39;
hence contradiction by A16, DIRAF:36; :: thesis: verum

end;

hence Mid p',a',b' by A13, A26, DIRAF:13; :: thesis: verum

end;

hence Mid p',a',b' by DIRAF:14; :: thesis: verum