let OAS be OAffinSpace; :: thesis: for a, b, a9, b9, c, c9 being Element of OAS st not LIN a,b,a9 & a,a9 '||' b,b9 & a,a9 '||' c,c9 & Mid a,b,c & LIN a9,b9,c9 holds
Mid a9,b9,c9
let a, b, a9, b9, c, c9 be Element of OAS; :: thesis: ( not LIN a,b,a9 & a,a9 '||' b,b9 & a,a9 '||' c,c9 & Mid a,b,c & LIN a9,b9,c9 implies Mid a9,b9,c9 )
assume that
A1: not LIN a,b,a9 and
A2: a,a9 '||' b,b9 and
A3: a,a9 '||' c,c9 and
A4: Mid a,b,c and
A5: LIN a9,b9,c9 ; :: thesis: Mid a9,b9,c9
A6: LIN a,b,c by A4, DIRAF:34;
A7: LIN b9,c9,a9 by A5, DIRAF:36;
A8: LIN c9,b9,a9 by A5, DIRAF:36;
A9: a <> a9 by A1, DIRAF:37;
then A10: b,b9 '||' c,c9 by A2, A3, DIRAF:28;
A11: a <> b by A1, DIRAF:37;
then A12: a <> c by A4, DIRAF:12;
A13: now
assume that
A14: b9 <> c9 and
a9 <> b9 and
A15: b <> b9 ; :: thesis: Mid a9,b9,c9
A16: not LIN b,b9,a9
proof
A17: LIN b,b9,b by DIRAF:37;
assume A18: LIN b,b9,a9 ; :: thesis: contradiction
b,b9 '||' a9,a by A2, DIRAF:27;
then LIN b,b9,a by A15, A18, DIRAF:39;
hence contradiction by A1, A15, A18, A17, DIRAF:38; :: thesis: verum
end;
A19: now
a,b '||' a,c by A6, DIRAF:def 5;
then c,a '||' a,b by DIRAF:27;
then consider x being Element of OAS such that
A20: c9,a '||' a,x and
A21: c9,c '||' b,x by A12, DIRAF:32;
a,c9 '||' a,x by A20, DIRAF:27;
then A22: LIN a,c9,x by DIRAF:def 5;
assume A23: c <> c9 ; :: thesis: Mid a9,b9,c9
A24: x <> b c,c9 '||' b,x by A21, DIRAF:27;
then b,b9 '||' b,x by A10, A23, DIRAF:28;
then A27: LIN b,b9,x by DIRAF:def 5;
then LIN b,x,b9 by DIRAF:36;
then b,x '||' b,b9 by DIRAF:def 5;
then b,x '||' c,c9 by A10, A15, DIRAF:28;
then A28: x,b '||' c,c9 by DIRAF:27;
A29: x <> b9
proof
assume x = b9 ; :: thesis: contradiction
then A30: LIN b9,c9,a by A22, DIRAF:36;
A31: a,a9 '||' b9,b by A2, DIRAF:27;
LIN b9,c9,b9 by DIRAF:37;
then LIN a,a9,b9 by A7, A14, A30, DIRAF:38;
then LIN a,a9,b by A9, A31, DIRAF:39;
hence contradiction by A1, DIRAF:36; :: thesis: verum
end;
A32: not LIN c9,b9,x
proof
assume LIN c9,b9,x ; :: thesis: contradiction
then A33: LIN b9,x,c9 by DIRAF:36;
A34: LIN b9,x,b9 by DIRAF:37;
A35: LIN c9,b9,b9 by DIRAF:37;
LIN b9,x,b by A27, DIRAF:36;
then LIN c9,b9,b by A29, A33, A34, DIRAF:38;
hence contradiction by A8, A14, A16, A35, DIRAF:38; :: thesis: verum
end;
A36: LIN x,b,b9 by A27, DIRAF:36;
A37: not LIN a,x,b
proof
assume LIN a,x,b ; :: thesis: contradiction
then A38: LIN x,b,a by DIRAF:36;
A39: b,b9 '||' a,a9 by A2, DIRAF:27;
LIN x,b,b by DIRAF:37;
then LIN b,b9,a by A36, A24, A38, DIRAF:38;
hence contradiction by A15, A16, A39, DIRAF:39; :: thesis: verum
end;
LIN b9,b,x by A27, DIRAF:36;
then b9,b '||' b9,x by DIRAF:def 5;
then b,b9 '||' b9,x by DIRAF:27;
then A40: b9,x '||' a,a9 by A2, A15, DIRAF:28;
LIN a,x,c9 by A22, DIRAF:36;
then Mid a,x,c9 by A4, A28, A37, Th15;
then Mid c9,x,a by DIRAF:13;
then Mid c9,b9,a9 by A8, A40, A32, Th15;
hence Mid a9,b9,c9 by DIRAF:13; :: thesis: verum
end;
( c = c9 implies Mid a9,b9,c9 )
proof
A41: not LIN c9,b9,b
proof
A42: LIN c9,b9,b9 by DIRAF:37;
assume LIN c9,b9,b ; :: thesis: contradiction
hence contradiction by A8, A14, A16, A42, DIRAF:38; :: thesis: verum
end;
assume c = c9 ; :: thesis: Mid a9,b9,c9
then A43: Mid c9,b,a by A4, DIRAF:13;
b9,b '||' a,a9 by A2, DIRAF:27;
then Mid c9,b9,a9 by A8, A43, A41, Th15;
hence Mid a9,b9,c9 by DIRAF:13; :: thesis: verum
end;
hence Mid a9,b9,c9 by A19; :: thesis: verum
end;
( b = b9 implies Mid a9,b9,c9 )
proof
A44: a,a9 '||' c9,c by A3, DIRAF:27;
A45: LIN b9,a9,c9 by A5, DIRAF:36;
assume A46: b = b9 ; :: thesis: Mid a9,b9,c9
then not LIN b9,a,a9 by A1, DIRAF:36;
hence Mid a9,b9,c9 by A4, A46, A45, A44, Th13; :: thesis: verum
end;
hence Mid a9,b9,c9 by A13, DIRAF:14; :: thesis: verum