let OAS be OAffinSpace; :: thesis: for p, a, b, p', a', b' being Element of 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 ; :: 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 by A3, DIRAF:37;
A8: p <> p' 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: p' <> b'

proof

assume A13: 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 A14: LIN p,b,b' 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,a'

proof

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

end;

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

A18: now

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

end;

assume that
A20: p' <> a' and
a' <> b' ; :: thesis: Mid p',a',b'
consider x being Element of such that
A21: Mid p,x,b' and
A22: b,b' // a,x by A1, Th26;
Mid b',x,p by A21, DIRAF:13;
then consider y being Element of such that
A23: Mid b',y,p' and
A24: p,p' // x,y by Th26;
LIN b',y,p' by A23, DIRAF:34;
then A25: LIN p',b',y by DIRAF:36;
A26: 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, A20, DIRAF:6;
then p,a '||' b,a' 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,b' by A21, DIRAF:34;
LIN p,a,a by DIRAF:37;
then A29: LIN b,b',a by A7, A9, A28, DIRAF:38;
LIN p,a,p by DIRAF:37;
then A30: LIN b,b',p by A7, A9, A28, 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 A26, A30, DIRAF:39;
hence contradiction by A3, A26, A29, A30, DIRAF:38; :: thesis: verum

end;

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

end;

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