let V be non trivial RealLinearSpace; ( ex x1, x2 being Element of st
( x1 <> x2 & ( for r1, r2 being Element of ex q being Element of st
( x1,x2,q is_collinear & r1,r2,q is_collinear ) ) ) implies for p, p1, q, q1 being Element of ex r being Element of st
( p,p1,r is_collinear & q,q1,r is_collinear ) )
given x1, x2 being Element of such that A1:
x1 <> x2
and
A2:
for r1, r2 being Element of ex q being Element of st
( x1,x2,q is_collinear & r1,r2,q is_collinear )
; for p, p1, q, q1 being Element of ex r being Element of st
( p,p1,r is_collinear & q,q1,r is_collinear )
let p, p1, q, q1 be Element of ; ex r being Element of st
( p,p1,r is_collinear & q,q1,r is_collinear )
consider p3 being Element of such that
A3:
x1,x2,p3 is_collinear
and
A4:
p,p1,p3 is_collinear
by A2;
consider q3 being Element of such that
A5:
x1,x2,q3 is_collinear
and
A6:
q,q1,q3 is_collinear
by A2;
consider s2 being Element of such that
A7:
x1,x2,s2 is_collinear
and
A8:
p,q,s2 is_collinear
by A2;
A9:
s2,p,q is_collinear
by A8, Th25;
consider s4 being Element of such that
A10:
x1,x2,s4 is_collinear
and
A11:
p,q1,s4 is_collinear
by A2;
A12:
s4,q1,p is_collinear
by A11, Th25;
p3,s2,q3 is_collinear
by A1, A3, A5, A7, Def8;
then consider s3 being Element of such that
A13:
p3,p,s3 is_collinear
and
A14:
q3,q,s3 is_collinear
by A9, Def9;
consider s being Element of such that
A15:
x1,x2,s is_collinear
and
A16:
p1,q1,s is_collinear
by A2;
q3,s4,p3 is_collinear
by A1, A3, A5, A10, Def8;
then consider s5 being Element of such that
A17:
q3,q1,s5 is_collinear
and
A18:
p3,p,s5 is_collinear
by A12, Def9;
A19:
p1,s,q1 is_collinear
by A16, Th25;
consider s6 being Element of such that
A20:
x1,x2,s6 is_collinear
and
A21:
p1,q,s6 is_collinear
by A2;
A22:
s6,p1,q is_collinear
by A21, Th25;
p3,s6,q3 is_collinear
by A1, A3, A5, A20, Def8;
then consider s7 being Element of such that
A23:
p3,p1,s7 is_collinear
and
A24:
q3,q,s7 is_collinear
by A22, Def9;
s,p3,q3 is_collinear
by A1, A3, A5, A15, Def8;
then consider s1 being Element of such that
A25:
p1,p3,s1 is_collinear
and
A26:
q1,q3,s1 is_collinear
by A19, Def9;
A27:
now A28:
now A29:
q3,
q1,
s1 is_collinear
by A26, Th25;
assume that A30:
p3 <> p1
and A31:
q3 <> q1
;
ex s1, r being Element of st
( p,p1,r is_collinear & q,q1,r is_collinear )
(
q3,
q1,
q is_collinear &
q3,
q1,
q1 is_collinear )
by A6, Def7, Th25;
then A32:
q,
q1,
s1 is_collinear
by A31, A29, Def8;
take s1 =
s1;
ex r being Element of st
( p,p1,r is_collinear & q,q1,r is_collinear )A33:
p3,
p1,
s1 is_collinear
by A25, Th25;
(
p3,
p1,
p is_collinear &
p3,
p1,
p1 is_collinear )
by A4, Def7, Th25;
then
p,
p1,
s1 is_collinear
by A30, A33, Def8;
hence
ex
r being
Element of st
(
p,
p1,
r is_collinear &
q,
q1,
r is_collinear )
by A32;
verum end; A34:
now assume that A35:
p3 <> p
and A36:
q3 <> q
;
ex s3, r being Element of st
( p,p1,r is_collinear & q,q1,r is_collinear )take s3 =
s3;
ex r being Element of st
( p,p1,r is_collinear & q,q1,r is_collinear )
(
q3,
q,
q is_collinear &
q3,
q,
q1 is_collinear )
by A6, Def7, Th25;
then A37:
q,
q1,
s3 is_collinear
by A14, A36, Def8;
(
p3,
p,
p is_collinear &
p3,
p,
p1 is_collinear )
by A4, Def7, Th25;
then
p,
p1,
s3 is_collinear
by A13, A35, Def8;
hence
ex
r being
Element of st
(
p,
p1,
r is_collinear &
q,
q1,
r is_collinear )
by A37;
verum end; A38:
now assume that A39:
p3 <> p1
and A40:
q3 <> q
;
ex s7, r being Element of st
( p,p1,r is_collinear & q,q1,r is_collinear )take s7 =
s7;
ex r being Element of st
( p,p1,r is_collinear & q,q1,r is_collinear )
(
q3,
q,
q is_collinear &
q3,
q,
q1 is_collinear )
by A6, Def7, Th25;
then A41:
q,
q1,
s7 is_collinear
by A24, A40, Def8;
(
p3,
p1,
p is_collinear &
p3,
p1,
p1 is_collinear )
by A4, Def7, Th25;
then
p,
p1,
s7 is_collinear
by A23, A39, Def8;
hence
ex
r being
Element of st
(
p,
p1,
r is_collinear &
q,
q1,
r is_collinear )
by A41;
verum end; A42:
now assume that A43:
p3 <> p
and A44:
q3 <> q1
;
ex s5, r being Element of st
( p,p1,r is_collinear & q,q1,r is_collinear )take s5 =
s5;
ex r being Element of st
( p,p1,r is_collinear & q,q1,r is_collinear )
(
q3,
q1,
q is_collinear &
q3,
q1,
q1 is_collinear )
by A6, Def7, Th25;
then A45:
q,
q1,
s5 is_collinear
by A17, A44, Def8;
(
p3,
p,
p is_collinear &
p3,
p,
p1 is_collinear )
by A4, Def7, Th25;
then
p,
p1,
s5 is_collinear
by A18, A43, Def8;
hence
ex
r being
Element of st
(
p,
p1,
r is_collinear &
q,
q1,
r is_collinear )
by A45;
verum end; assume
(
p <> p1 &
q <> q1 )
;
ex r being Element of st
( p,p1,r is_collinear & q,q1,r is_collinear )hence
ex
r being
Element of st
(
p,
p1,
r is_collinear &
q,
q1,
r is_collinear )
by A34, A42, A38, A28;
verum
now A46:
now assume A47:
p = p1
;
ex q3, r being Element of st
( p,p1,r is_collinear & q,q1,r is_collinear )take q3 =
q3;
ex r being Element of st
( p,p1,r is_collinear & q,q1,r is_collinear )
p,
p1,
q3 is_collinear
by A47, Def7;
hence
ex
r being
Element of st
(
p,
p1,
r is_collinear &
q,
q1,
r is_collinear )
by A6;
verum end; A48:
now assume A49:
q = q1
;
ex p3, r being Element of st
( p,p1,r is_collinear & q,q1,r is_collinear )take p3 =
p3;
ex r being Element of st
( p,p1,r is_collinear & q,q1,r is_collinear )
q,
q1,
p3 is_collinear
by A49, Def7;
hence
ex
r being
Element of st
(
p,
p1,
r is_collinear &
q,
q1,
r is_collinear )
by A4;
verum end; assume
(
p = p1 or
q = q1 )
;
ex r being Element of st
( p,p1,r is_collinear & q,q1,r is_collinear )hence
ex
r being
Element of st
(
p,
p1,
r is_collinear &
q,
q1,
r is_collinear )
by A48, A46;
verum
hence
ex r being Element of st
( p,p1,r is_collinear & q,q1,r is_collinear )
by A27; verum