let OAS be OAffinSpace; :: thesis: for a, b, c being Element of OAS ex x being Element of OAS st
( a,x // b,c & a,b // x,c )
let a, b, c be Element of OAS; :: thesis: ex x being Element of OAS st
( a,x // b,c & a,b // x,c )

A1: now

assume A2: LIN a,b,c ; :: thesis: ex x being Element of OAS st
( a,x // b,c & a,b // x,c )
A3: ( Mid a,b,c implies ( a,b // b,c & a,b // b,c ) ) by DIRAF:def 3;

A4: now

assume Mid b,a,c ; :: thesis: ( a,c // b,c & a,b // c,c )
then Mid c,a,b by DIRAF:13;
then c,a // a,b by DIRAF:def 3;
then c,a // c,b by ANALOAF:def 5;
hence ( a,c // b,c & a,b // c,c ) by DIRAF:5, DIRAF:7; :: thesis: verum

end;

now

assume Mid a,c,b ; :: thesis: ( a,a // b,c & a,b // a,c )
then a,c // c,b by DIRAF:def 3;
then a,c // a,b by ANALOAF:def 5;
hence ( a,a // b,c & a,b // a,c ) by DIRAF:5, DIRAF:7; :: thesis: verum

end;

hence ex x being Element of OAS st
( a,x // b,c & a,b // x,c ) by A2, A3, A4, DIRAF:35; :: thesis: verum

end;

now

assume A5: not LIN a,b,c ; :: thesis: ex x being Element of OAS st
( a,x // b,c & a,b // x,c )
then A6: ( a <> b & a <> c & b <> c ) by DIRAF:37;
consider e1 being Element of OAS such that
A7: ( Mid c,a,e1 & a <> e1 ) by DIRAF:17;
A8: c,a // a,e1 by A7, DIRAF:def 3;
then consider e2 being Element of OAS such that
A9: ( b,a // a,e2 & b,c // e1,e2 ) by A6, ANALOAF:def 5;
consider e3 being Element of OAS such that
A10: ( Mid b,c,e3 & c <> e3 ) by DIRAF:17;
A11: b,c // c,e3 by A10, DIRAF:def 3;
then consider e4 being Element of OAS such that
A12: ( a,c // c,e4 & a,b // e3,e4 ) by A6, ANALOAF:def 5;
Mid a,c,e4 by A12, DIRAF:def 3;
then A13: Mid e4,c,a by DIRAF:13;
then ( e4,c // c,a & c,a // c,e1 ) by A8, ANALOAF:def 5, DIRAF:def 3;
then e4,c // c,e1 by A6, DIRAF:6;
then A14: Mid e4,c,e1 by DIRAF:def 3;
then A15: Mid e1,c,e4 by DIRAF:13;
A16: e4 <> c

proof

assume e4 = c ; :: thesis: contradiction
then ( a,b // e3,c & e3,c // c,b ) by A11, A12, DIRAF:5;
then a,b // c,b by A10, 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 A5, DIRAF:36; :: thesis: verum

end;

then consider e5 being Element of OAS such that
A17: ( Mid e4,e3,e5 & c,e3 // e1,e5 ) by A14, Th27;
A18: e4 <> e3

proof

assume e4 = e3 ; :: thesis: contradiction
then Mid a,c,e3 by A12, DIRAF:def 3;
then ( LIN e3,c,a & Mid e3,c,b ) by A10, DIRAF:13, DIRAF:34;
then ( LIN e3,c,a & LIN e3,c,b & LIN e3,c,c ) by DIRAF:34, DIRAF:37;
hence contradiction by A5, A10, DIRAF:38; :: thesis: verum

end;

then A19: e4 <> e5 by A17, DIRAF:12;
A20: e1 <> e4 by A14, A16, DIRAF:12;
A21: not LIN e4,c,e3

proof

assume LIN e4,c,e3 ; :: thesis: contradiction
then ( LIN e4,c,e3 & LIN e4,c,a & LIN e4,c,c ) by A13, DIRAF:34, DIRAF:37;
then ( LIN c,e3,a & LIN b,c,e3 ) by A10, A16, DIRAF:34, DIRAF:38;
then ( LIN c,e3,a & LIN c,e3,b & LIN c,e3,c ) by DIRAF:36, DIRAF:37;
hence contradiction by A5, A10, DIRAF:38; :: thesis: verum

end;

A22: not LIN e1,e4,e3

proof

assume LIN e1,e4,e3 ; :: thesis: contradiction
then ( LIN e1,e4,e3 & LIN e4,c,e1 ) by A14, DIRAF:34;
then ( LIN e4,e1,e3 & LIN e4,e1,c & LIN e4,e1,e4 ) by DIRAF:36, DIRAF:37;
hence contradiction by A20, A21, DIRAF:38; :: thesis: verum

end;

A23: not LIN e1,e5,e4

proof

assume LIN e1,e5,e4 ; :: thesis: contradiction
then ( LIN e5,e4,e1 & LIN e4,e3,e5 ) by A17, DIRAF:34, DIRAF:36;
then ( LIN e5,e4,e1 & LIN e5,e4,e3 & LIN e5,e4,e4 ) by DIRAF:36, DIRAF:37;
hence contradiction by A19, A22, DIRAF:38; :: thesis: verum

end;

then consider e6 being Element of OAS such that
A24: ( Mid e1,e6,e5 & e5,e4 // e6,c ) by A15, Th28;
consider x being Element of OAS such that
A25: ( Mid c,x,e6 & e1,e6 // a,x ) by A7, Th26;
A26: e1 <> e5 by A23, DIRAF:37;
A27: c <> e1 by A7, DIRAF:12;
A28: not LIN c,e1,b

proof

assume LIN c,e1,b ; :: thesis: contradiction
then ( LIN c,e1,b & LIN c,a,e1 ) by A7, DIRAF:34;
then ( LIN c,e1,b & LIN c,e1,a & LIN c,e1,c ) by DIRAF:36, DIRAF:37;
hence contradiction by A5, A27, DIRAF:38; :: thesis: verum

end;

A29: e5 <> e3

proof

assume e5 = e3 ; :: thesis: contradiction
then e3,c // e3,e1 by A17, DIRAF:5;
then ( Mid e3,c,e1 or Mid e3,e1,c ) by DIRAF:11;
then ( LIN e3,c,e1 or LIN e3,e1,c ) by DIRAF:34;
then ( LIN e3,c,e1 & Mid e3,c,b ) by A10, DIRAF:13, DIRAF:36;
then ( LIN e3,c,e1 & LIN e3,c,b & LIN e3,c,c ) by DIRAF:34, DIRAF:37;
hence contradiction by A10, A28, DIRAF:38; :: thesis: verum

end;

A30: e1 <> e6

proof

assume A31: e1 = e6 ; :: thesis: contradiction
Mid e5,e3,e4 by A17, DIRAF:13;
then e5,e3 // e3,e4 by DIRAF:def 3;
then ( e5,e3 // e3,e4 & e5,e3 // e5,e4 ) by ANALOAF:def 5;
then e5,e4 // e3,e4 by A29, ANALOAF:def 5;
then e3,e4 // e1,c by A19, A24, A31, ANALOAF:def 5;
then ( a,b // e1,c & Mid e1,a,c ) by A7, A12, A18, DIRAF:6, DIRAF:13;
then ( a,b // e1,c & e1,a // a,c ) by DIRAF:def 3;
then ( a,b // e1,c & e1,a // a,c & e1,a // e1,c ) by ANALOAF:def 5;
then ( a,b // e1,c & e1,c // a,c ) by A7, ANALOAF:def 5;
then a,b // a,c by A27, DIRAF:6;
then ( a,b // b,c or a,c // c,b ) by DIRAF:9;
then ( Mid a,b,c or Mid a,c,b ) by DIRAF:def 3;
then ( LIN a,b,c or LIN a,c,b ) by DIRAF:34;
hence contradiction by A5, DIRAF:36; :: thesis: verum

end;

e1,e6 // e6,e5 by A24, DIRAF:def 3;
then e1,e6 // e1,e5 by ANALOAF:def 5;
then e1,e5 // a,x by A25, A30, ANALOAF:def 5;
then ( c,e3 // a,x & b,c // c,e3 ) by A10, A17, A26, DIRAF:6, DIRAF:def 3;
then ( c,e3 // a,x & c,e3 // b,c ) by DIRAF:5;
then A32: a,x // b,c by A10, ANALOAF:def 5;
Mid e5,e3,e4 by A17, DIRAF:13;
then e5,e3 // e3,e4 by DIRAF:def 3;
then ( e5,e3 // e3,e4 & e5,e3 // e5,e4 ) by ANALOAF:def 5;
then e3,e4 // e5,e4 by A29, ANALOAF:def 5;
then a,b // e5,e4 by A12, A18, DIRAF:6;
then A33: a,b // e6,c by A19, A24, DIRAF:6;
A34: e6 <> c

proof

assume e6 = c ; :: thesis: contradiction
then x = c by A25, DIRAF:12;
then c,a // c,b by A32, DIRAF:5;
then ( Mid c,a,b or Mid c,b,a ) by DIRAF:11;
then ( LIN c,a,b or LIN c,b,a ) by DIRAF:34;
hence contradiction by A5, DIRAF:36; :: thesis: verum

end;

A35: a <> e2

proof

assume a = e2 ; :: thesis: contradiction
then ( b,c // e1,a & e1,a // a,c ) by A8, A9, DIRAF:5;
then b,c // a,c by A7, DIRAF:6;
then c,b // c,a by DIRAF:5;
then ( Mid c,b,a or Mid c,a,b ) by DIRAF:11;
then ( LIN c,b,a or LIN c,a,b ) by DIRAF:34;
hence contradiction by A5, DIRAF:36; :: thesis: verum

end;

A36: e6 <> x

proof

assume e6 = x ; :: thesis: contradiction
then e6,e1 // e6,a by A25, DIRAF:5;
then ( Mid e6,e1,a or Mid e6,a,e1 ) by DIRAF:11;
then ( LIN e6,e1,a or LIN e6,a,e1 ) by DIRAF:34;
then ( LIN e6,e1,a & LIN e1,e6,e5 ) by A24, DIRAF:34, DIRAF:36;
then ( LIN e6,e1,a & LIN e6,e1,e5 & LIN e6,e1,e1 ) by DIRAF:36, DIRAF:37;
then A37: LIN e1,e5,a by A30, DIRAF:38;
b,c // e1,e5 by A10, A11, A17, DIRAF:6;
then e1,e2 // e1,e5 by A6, A9, ANALOAF:def 5;
then ( Mid e1,e2,e5 or Mid e1,e5,e2 ) by DIRAF:11;
then ( LIN e1,e2,e5 or LIN e1,e5,e2 ) by DIRAF:34;
then ( LIN e1,e5,e2 & LIN e1,e5,e1 ) by DIRAF:36, DIRAF:37;
then ( LIN a,e1,e2 & LIN c,a,e1 ) by A7, A26, A37, DIRAF:34, DIRAF:38;
then ( LIN a,e1,e2 & LIN a,e1,c & LIN a,e1,a ) by DIRAF:36, DIRAF:37;
then ( LIN a,e2,c & Mid b,a,e2 ) by A7, A9, DIRAF:38, DIRAF:def 3;
then ( LIN a,e2,c & LIN b,a,e2 ) by DIRAF:34;
then ( LIN a,e2,c & LIN a,e2,b & LIN a,e2,a ) by DIRAF:36, DIRAF:37;
hence contradiction by A5, A35, DIRAF:38; :: thesis: verum

end;

Mid e6,x,c by A25, DIRAF:13;
then e6,x // x,c by DIRAF:def 3;
then ( e6,x // x,c & e6,x // e6,c ) by ANALOAF:def 5;
then e6,c // x,c by A36, ANALOAF:def 5;
then a,b // x,c by A33, A34, DIRAF:6;
hence ex x being Element of OAS st
( a,x // b,c & a,b // x,c ) by A32; :: thesis: verum

end;

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