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