let OAS be OAffinSpace; for a, a9, b, b9, c, c9 being Element of OAS st not a,b,a9 are_collinear & a,a9 '||' b,b9 & a,a9 '||' c,c9 & Mid a,b,c & a9,b9,c9 are_collinear holds
Mid a9,b9,c9
let a, a9, b, b9, c, c9 be Element of OAS; ( not a,b,a9 are_collinear & a,a9 '||' b,b9 & a,a9 '||' c,c9 & Mid a,b,c & a9,b9,c9 are_collinear implies Mid a9,b9,c9 )
assume that
A1:
not a,b,a9 are_collinear
and
A2:
a,a9 '||' b,b9
and
A3:
a,a9 '||' c,c9
and
A4:
Mid a,b,c
and
A5:
a9,b9,c9 are_collinear
; Mid a9,b9,c9
A6:
a,b,c are_collinear
by A4, DIRAF:28;
A7:
b9,c9,a9 are_collinear
by A5, DIRAF:30;
A8:
c9,b9,a9 are_collinear
by A5, DIRAF:30;
A9:
a <> a9
by A1, DIRAF:31;
then A10:
b,b9 '||' c,c9
by A2, A3, DIRAF:23;
A11:
a <> b
by A1, DIRAF:31;
then A12:
a <> c
by A4, DIRAF:8;
A13:
now ( b9 <> c9 & a9 <> b9 & b <> b9 implies Mid a9,b9,c9 )assume that A14:
b9 <> c9
and
a9 <> b9
and A15:
b <> b9
;
Mid a9,b9,c9A16:
not
b,
b9,
a9 are_collinear
proof
A17:
b,
b9,
b are_collinear
by DIRAF:31;
assume A18:
b,
b9,
a9 are_collinear
;
contradiction
b,
b9 '||' a9,
a
by A2, DIRAF:22;
then
b,
b9,
a are_collinear
by A15, A18, DIRAF:33;
hence
contradiction
by A1, A15, A18, A17, DIRAF:32;
verum
end; A19:
now ( c <> c9 implies Mid a9,b9,c9 )
a,
b '||' a,
c
by A6, DIRAF:def 5;
then
c,
a '||' a,
b
by DIRAF:22;
then consider x being
Element of
OAS such that A20:
c9,
a '||' a,
x
and A21:
c9,
c '||' b,
x
by A12, DIRAF:27;
a,
c9 '||' a,
x
by A20, DIRAF:22;
then A22:
a,
c9,
x are_collinear
by DIRAF:def 5;
assume A23:
c <> c9
;
Mid a9,b9,c9A24:
x <> b
proof
assume
x = b
;
contradiction
then A25:
a,
b,
c9 are_collinear
by A22, DIRAF:30;
a,
b,
b are_collinear
by DIRAF:31;
then A26:
c,
c9,
b are_collinear
by A11, A6, A25, DIRAF:32;
a,
b,
a are_collinear
by DIRAF:31;
then
c,
c9,
a are_collinear
by A11, A6, A25, DIRAF:32;
then
c,
c9 '||' a,
b
by A26, DIRAF:34;
then
b,
b9 '||' a,
b
by A10, A23, DIRAF:23;
then
a,
a9 '||' a,
b
by A2, A15, DIRAF:23;
then
a,
a9,
b are_collinear
by DIRAF:def 5;
hence
contradiction
by A1, DIRAF:30;
verum
end;
c,
c9 '||' b,
x
by A21, DIRAF:22;
then
b,
b9 '||' b,
x
by A10, A23, DIRAF:23;
then A27:
b,
b9,
x are_collinear
by DIRAF:def 5;
then
b,
x,
b9 are_collinear
by DIRAF:30;
then
b,
x '||' b,
b9
by DIRAF:def 5;
then
b,
x '||' c,
c9
by A10, A15, DIRAF:23;
then A28:
x,
b '||' c,
c9
by DIRAF:22;
A29:
x <> b9
proof
assume
x = b9
;
contradiction
then A30:
b9,
c9,
a are_collinear
by A22, DIRAF:30;
A31:
a,
a9 '||' b9,
b
by A2, DIRAF:22;
b9,
c9,
b9 are_collinear
by DIRAF:31;
then
a,
a9,
b9 are_collinear
by A7, A14, A30, DIRAF:32;
then
a,
a9,
b are_collinear
by A9, A31, DIRAF:33;
hence
contradiction
by A1, DIRAF:30;
verum
end; A32:
not
c9,
b9,
x are_collinear
proof
assume
c9,
b9,
x are_collinear
;
contradiction
then A33:
b9,
x,
c9 are_collinear
by DIRAF:30;
A34:
b9,
x,
b9 are_collinear
by DIRAF:31;
A35:
c9,
b9,
b9 are_collinear
by DIRAF:31;
b9,
x,
b are_collinear
by A27, DIRAF:30;
then
c9,
b9,
b are_collinear
by A29, A33, A34, DIRAF:32;
hence
contradiction
by A8, A14, A16, A35, DIRAF:32;
verum
end; A36:
x,
b,
b9 are_collinear
by A27, DIRAF:30;
A37:
not
a,
x,
b are_collinear
proof
assume
a,
x,
b are_collinear
;
contradiction
then A38:
x,
b,
a are_collinear
by DIRAF:30;
A39:
b,
b9 '||' a,
a9
by A2, DIRAF:22;
x,
b,
b are_collinear
by DIRAF:31;
then
b,
b9,
a are_collinear
by A36, A24, A38, DIRAF:32;
hence
contradiction
by A15, A16, A39, DIRAF:33;
verum
end;
b9,
b,
x are_collinear
by A27, DIRAF:30;
then
b9,
b '||' b9,
x
by DIRAF:def 5;
then
b,
b9 '||' b9,
x
by DIRAF:22;
then A40:
b9,
x '||' a,
a9
by A2, A15, DIRAF:23;
a,
x,
c9 are_collinear
by A22, DIRAF:30;
then
Mid a,
x,
c9
by A4, A28, A37, Th8;
then
Mid c9,
x,
a
by DIRAF:9;
then
Mid c9,
b9,
a9
by A8, A40, A32, Th8;
hence
Mid a9,
b9,
c9
by DIRAF:9;
verum end;
(
c = c9 implies
Mid a9,
b9,
c9 )
proof
A41:
not
c9,
b9,
b are_collinear
assume
c = c9
;
Mid a9,b9,c9
then A43:
Mid c9,
b,
a
by A4, DIRAF:9;
b9,
b '||' a,
a9
by A2, DIRAF:22;
then
Mid c9,
b9,
a9
by A8, A43, A41, Th8;
hence
Mid a9,
b9,
c9
by DIRAF:9;
verum
end; hence
Mid a9,
b9,
c9
by A19;
verum end;
( b = b9 implies Mid a9,b9,c9 )
proof
A44:
a,
a9 '||' c9,
c
by A3, DIRAF:22;
A45:
b9,
a9,
c9 are_collinear
by A5, DIRAF:30;
assume A46:
b = b9
;
Mid a9,b9,c9
then
not
b9,
a,
a9 are_collinear
by A1, DIRAF:30;
hence
Mid a9,
b9,
c9
by A4, A46, A45, A44, Th6;
verum
end;
hence
Mid a9,b9,c9
by A13, DIRAF:10; verum