let OAS be OAffinSpace; for a, a9, b, b9, p being Element of OAS st not p,a,a9 are_collinear & p,a // p,b & p,a9 // p,b9 & a,a9 '||' b,b9 holds
a,a9 // b,b9
let a, a9, b, b9, p be Element of OAS; ( not p,a,a9 are_collinear & p,a // p,b & p,a9 // p,b9 & a,a9 '||' b,b9 implies a,a9 // b,b9 )
assume that
A1:
not p,a,a9 are_collinear
and
A2:
p,a // p,b
and
A3:
p,a9 // p,b9
and
A4:
a,a9 '||' b,b9
; a,a9 // b,b9
consider c being Element of OAS such that
A5:
Mid a,p,c
and
A6:
p <> c
by DIRAF:13;
A7:
a,p // p,c
by A5, DIRAF:def 3;
A8:
a <> p
by A1, DIRAF:31;
then consider c9 being Element of OAS such that
A9:
a9,p // p,c9
and
A10:
a9,a // c,c9
by A7, ANALOAF:def 5;
A11:
a9,a '||' c9,c
by A10, DIRAF:def 4;
A12:
c <> c9
proof
assume
c = c9
;
contradiction
then
Mid a9,
p,
c
by A9, DIRAF:def 3;
then
a9,
p,
c are_collinear
by DIRAF:28;
then A13:
p,
c,
a9 are_collinear
by DIRAF:30;
a,
p,
c are_collinear
by A5, DIRAF:28;
then A14:
p,
c,
a are_collinear
by DIRAF:30;
p,
c,
p are_collinear
by DIRAF:31;
hence
contradiction
by A1, A6, A14, A13, DIRAF:32;
verum
end;
p,a // c,p
by A7, DIRAF:2;
then
c,p // p,b
by A2, A8, ANALOAF:def 5;
then consider b99 being Element of OAS such that
A15:
c9,p // p,b99
and
A16:
c9,c // b,b99
by A6, ANALOAF:def 5;
A17:
a9,a '||' b,b9
by A4, DIRAF:22;
A18:
p <> c9
proof
assume
p = c9
;
contradiction
then
a9,
a '||' c,
p
by A10, DIRAF:def 4;
then A19:
p,
c '||' a,
a9
by DIRAF:22;
a,
p '||' p,
c
by A7, DIRAF:def 4;
then
a,
p '||' a,
a9
by A6, A19, DIRAF:23;
then
a,
p,
a9 are_collinear
by DIRAF:def 5;
hence
contradiction
by A1, DIRAF:30;
verum
end;
p,a '||' p,b
by A2, DIRAF:def 4;
then A20:
p,a,b are_collinear
by DIRAF:def 5;
A21:
c9,c // a,a9
by A10, DIRAF:2;
a9,p '||' p,c9
by A9, DIRAF:def 4;
then A22:
p,a9 '||' p,c9
by DIRAF:22;
p,a9 '||' p,b9
by A3, DIRAF:def 4;
then A23:
p,a9,b9 are_collinear
by DIRAF:def 5;
c9,p '||' p,b99
by A15, DIRAF:def 4;
then
p,c9 '||' p,b99
by DIRAF:22;
then
p,a9 '||' p,b99
by A18, A22, DIRAF:23;
then A24:
p,a9,b99 are_collinear
by DIRAF:def 5;
c9,c '||' b,b99
by A16, DIRAF:def 4;
then A25:
a9,a '||' b,b99
by A12, A11, DIRAF:23;
not p,a9,a are_collinear
by A1, DIRAF:30;
then
c9,c // b,b9
by A20, A23, A17, A16, A24, A25, Th4;
hence
a,a9 // b,b9
by A12, A21, ANALOAF:def 5; verum