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