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 that
A1: a,b // c,d and
A2: not LIN a,b,c ; :: thesis: ex x being Element of OAS st
( Mid a,x,d & Mid b,x,c )

A3: now

consider e1 being Element of OAS such that
A4: a,b // d,e1 and
A5: a,d // b,e1 and
A6: b <> e1 by ANALOAF:def 5;
A7: a <> b by A2, DIRAF:37;
then c,d // d,e1 by A1, A4, ANALOAF:def 5;
then A8: Mid c,d,e1 by DIRAF:def 3;
A9: 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 A2, DIRAF:36; :: thesis: verum

end;

A10: not LIN a,b,d

proof

A11: 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;

A12: LIN d,a,a by DIRAF:37;

A13: 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;

assume A14: LIN a,b,d ; :: thesis: contradiction
then A15: LIN d,a,b by DIRAF:36;
a,b '||' a,d by A14, DIRAF:def 5;
then LIN d,a,c by A11, A13, DIRAF:36, DIRAF:def 4;
hence contradiction by A2, A9, A12, A15, DIRAF:38; :: thesis: verum

end;

consider e2 being Element of OAS such that
A16: c,d // b,e2 and
A17: c,b // d,e2 and
A18: d <> e2 by ANALOAF:def 5;
assume A19: c <> d ; :: thesis: ex x being Element of OAS st
( Mid a,x,d & Mid b,x,c )
then a,b // b,e2 by A1, A16, DIRAF:6;
then A20: Mid a,b,e2 by DIRAF:def 3;
A21: not LIN c,d,b

proof

A22: now

assume c,d // c,b ; :: thesis: contradiction
then a,b // c,b by A1, A19, 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 A2, DIRAF:36; :: thesis: verum

end;

assume LIN c,d,b ; :: thesis: contradiction
then c,d '||' c,b by DIRAF:def 5;
then ( c,d // c,b or c,d // b,c ) by DIRAF:def 4;
then a,b // b,c by A1, A19, A22, DIRAF:6;
then Mid a,b,c by DIRAF:def 3;
hence contradiction by A2, DIRAF:34; :: thesis: verum

end;

A23: LIN b,c,c by DIRAF:37;
A24: LIN d,a,a by DIRAF:37;
A25: c <> e1

proof

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

end;

not LIN c,b,e1

proof

LIN c,d,e1 by A8, DIRAF:34;
then A26: LIN c,e1,d by DIRAF:36;
assume LIN c,b,e1 ; :: thesis: contradiction
then A27: LIN c,e1,b by DIRAF:36;
LIN c,e1,c by DIRAF:37;
hence contradiction by A25, A21, A27, A26, DIRAF:38; :: thesis: verum

end;

then consider x being Element of OAS such that
A28: Mid c,x,b and
A29: b,e1 // x,d by A8, Th28;
A30: Mid b,x,c by A28, DIRAF:13;
a,d // x,d by A5, A6, A29, 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 A31: LIN d,a,x by DIRAF:36;
A32: b <> c by A2, DIRAF:37;
A33: a <> e2

proof

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

end;

not LIN a,d,e2

proof

LIN a,b,e2 by A20, DIRAF:34;
then A34: LIN a,e2,b by DIRAF:36;
assume LIN a,d,e2 ; :: thesis: contradiction
then A35: LIN a,e2,d by DIRAF:36;
LIN a,e2,a by DIRAF:37;
hence contradiction by A33, A10, A35, A34, DIRAF:38; :: thesis: verum

end;

then consider y being Element of OAS such that
A36: Mid a,y,d and
A37: d,e2 // y,b by A20, Th28;
A38: LIN b,c,b by DIRAF:37;
c,b // y,b by A17, A18, A37, 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 A39: LIN b,c,y by DIRAF:36;
A40: LIN c,x,b by A28, DIRAF:34;
then LIN b,c,x by DIRAF:36;
then A41: LIN x,y,c by A32, A39, A23, DIRAF:38;
LIN a,y,d by A36, DIRAF:34;
then LIN d,a,y by DIRAF:36;
then A42: LIN x,y,a by A9, A31, A24, DIRAF:38;
LIN b,c,x by A40, DIRAF:36;
then LIN x,y,b by A32, A39, A38, DIRAF:38;
then Mid a,x,d by A2, A36, A42, A41, DIRAF:38;
hence ex x being Element of OAS st
( Mid a,x,d & Mid b,x,c ) by A30; :: thesis: verum

end;

now

assume A43: 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 A43, DIRAF:14; :: thesis: verum

end;

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