let OAS be OAffinSpace; :: thesis: for a, b, c, d being Element of OAS st a,b // c,d & not LIN a,b,c holds
ex x being Element of OAS st
( Mid a,x,d & Mid b,x,c )
let a, b, c, d be Element of OAS; :: thesis: ( a,b // c,d & not LIN a,b,c implies ex x being Element of OAS st
( Mid a,x,d & Mid b,x,c ) )
assume A1: ( a,b // c,d & not LIN a,b,c ) ; :: thesis: ex x being Element of OAS st
( Mid a,x,d & Mid b,x,c )

A2: now

assume A3: c = d ; :: thesis: ex x being Element of OAS st
( Mid a,x,d & Mid b,x,c )
take x = c; :: thesis: ( Mid a,x,d & Mid b,x,c )
thus ( Mid a,x,d & Mid b,x,c ) by A3, DIRAF:14; :: thesis: verum

end;

now

assume A4: c <> d ; :: thesis: ex x being Element of OAS st
( Mid a,x,d & Mid b,x,c )
consider e1 being Element of OAS such that
A5: ( a,b // d,e1 & a,d // b,e1 & b <> e1 ) by ANALOAF:def 5;
consider e2 being Element of OAS such that
A6: ( c,d // b,e2 & c,b // d,e2 & d <> e2 ) by ANALOAF:def 5;
A7: ( a <> b & b <> c ) by A1, DIRAF:37;
then c,d // d,e1 by A1, A5, ANALOAF:def 5;
then A8: Mid c,d,e1 by DIRAF:def 3;
a,b // b,e2 by A1, A4, A6, DIRAF:6;
then A9: Mid a,b,e2 by DIRAF:def 3;
A10: c <> e1

proof

assume c = e1 ; :: thesis: contradiction
then c,d // d,c by A1, A5, A7, ANALOAF:def 5;
hence contradiction by A4, ANALOAF:def 5; :: thesis: verum

end;

A11: a <> e2

proof

assume a = e2 ; :: thesis: contradiction
then a,b // b,a by A1, A4, A6, DIRAF:6;
hence contradiction by A7, ANALOAF:def 5; :: thesis: verum

end;

A12: a <> d

proof

assume a = d ; :: thesis: contradiction
then b,a // a,c by A1, DIRAF:5;
then Mid b,a,c by DIRAF:def 3;
then LIN b,a,c by DIRAF:34;
hence contradiction by A1, DIRAF:36; :: thesis: verum

end;

A13: not LIN c,d,b

proof

assume LIN c,d,b ; :: thesis: contradiction
then c,d '||' c,b by DIRAF:def 5;
then A14: ( c,d // c,b or c,d // b,c ) by DIRAF:def 4;

now

assume c,d // c,b ; :: thesis: contradiction
then a,b // c,b by A1, A4, DIRAF:6;
then b,a // b,c by DIRAF:5;
then ( Mid b,a,c or Mid b,c,a ) by DIRAF:11;
then ( LIN b,a,c or LIN b,c,a ) by DIRAF:34;
hence contradiction by A1, DIRAF:36; :: thesis: verum

end;

then a,b // b,c by A1, A4, A14, DIRAF:6;
then Mid a,b,c by DIRAF:def 3;
hence contradiction by A1, DIRAF:34; :: thesis: verum

end;

A15: not LIN a,b,d

proof

assume A16: LIN a,b,d ; :: thesis: contradiction
then A17: a,b '||' a,d by DIRAF:def 5;

A18: now

assume a,b // a,d ; :: thesis: LIN d,c,a
then c,d // a,d by A1, A7, ANALOAF:def 5;
then d,c // d,a by DIRAF:5;
then d,c '||' d,a by DIRAF:def 4;
hence LIN d,c,a by DIRAF:def 5; :: thesis: verum

end;

now

assume a,b // d,a ; :: thesis: LIN d,c,a
then c,d // d,a by A1, A7, ANALOAF:def 5;
then Mid c,d,a by DIRAF:def 3;
then LIN c,d,a by DIRAF:34;
hence LIN d,c,a by DIRAF:36; :: thesis: verum

end;

then ( LIN d,a,a & LIN d,a,c & LIN d,a,b ) by A16, A17, A18, DIRAF:36, DIRAF:37, DIRAF:def 4;
hence contradiction by A1, A12, DIRAF:38; :: thesis: verum

end;

A19: not LIN c,b,e1

proof

assume LIN c,b,e1 ; :: thesis: contradiction
then ( LIN c,e1,b & LIN c,d,e1 ) by A8, DIRAF:34, DIRAF:36;
then ( LIN c,e1,b & LIN c,e1,d & LIN c,e1,c ) by DIRAF:36, DIRAF:37;
hence contradiction by A10, A13, DIRAF:38; :: thesis: verum

end;

A20: not LIN a,d,e2

proof

assume LIN a,d,e2 ; :: thesis: contradiction
then ( LIN a,e2,d & LIN a,b,e2 ) by A9, DIRAF:34, DIRAF:36;
then ( LIN a,e2,d & LIN a,e2,b & LIN a,e2,a ) by DIRAF:36, DIRAF:37;
hence contradiction by A11, A15, DIRAF:38; :: thesis: verum

end;

consider x being Element of OAS such that
A21: ( Mid c,x,b & b,e1 // x,d ) by A8, A19, Th28;
consider y being Element of OAS such that
A22: ( Mid a,y,d & d,e2 // y,b ) by A9, A20, Th28;
c,b // y,b by A6, A22, DIRAF:6;
then b,c // b,y by DIRAF:5;
then ( Mid b,c,y or Mid b,y,c ) by DIRAF:11;
then ( LIN b,c,y or LIN b,y,c ) by DIRAF:34;
then A23: LIN b,c,y by DIRAF:36;
a,d // x,d by A5, A21, DIRAF:6;
then d,a // d,x by DIRAF:5;
then ( Mid d,a,x or Mid d,x,a ) by DIRAF:11;
then ( LIN d,a,x or LIN d,x,a ) by DIRAF:34;
then A24: LIN d,a,x by DIRAF:36;
A25: LIN c,x,b by A21, DIRAF:34;
then A26: LIN b,c,x by DIRAF:36;
( LIN b,c,x & LIN b,c,b ) by A25, DIRAF:36, DIRAF:37;
then A27: LIN x,y,b by A7, A23, DIRAF:38;
LIN a,y,d by A22, DIRAF:34;
then ( LIN d,a,y & LIN d,a,a ) by DIRAF:36, DIRAF:37;
then A28: LIN x,y,a by A12, A24, DIRAF:38;
LIN b,c,c by DIRAF:37;
then LIN x,y,c by A7, A23, A26, DIRAF:38;
then ( Mid a,x,d & Mid b,x,c ) by A1, A21, A22, A27, A28, DIRAF:13, DIRAF:38;
hence ex x being Element of OAS st
( Mid a,x,d & Mid b,x,c ) ; :: thesis: verum

end;

hence ex x being Element of OAS st
( Mid a,x,d & Mid b,x,c ) by A2; :: thesis: verum