let V be non trivial RealLinearSpace; ( ProjectiveSpace V is proper & ProjectiveSpace V is at_least_3rank & ex p, q1, q2 being Element of (ProjectiveSpace V) st
( not p,q1,q2 are_collinear & ( for r1, r2 being Element of (ProjectiveSpace V) ex q3, r3 being Element of (ProjectiveSpace V) st
( r1,r2,r3 are_collinear & q1,q2,q3 are_collinear & p,r3,q3 are_collinear ) ) ) implies ex CS being CollProjectiveSpace st
( CS = ProjectiveSpace V & CS is at_most-3-dimensional ) )
assume that
A1:
ProjectiveSpace V is proper
and
A2:
for p, q being Element of (ProjectiveSpace V) ex r being Element of (ProjectiveSpace V) st
( p <> r & q <> r & p,q,r are_collinear )
; ANPROJ_2:def 10 ( for p, q1, q2 being Element of (ProjectiveSpace V) holds
( p,q1,q2 are_collinear or ex r1, r2 being Element of (ProjectiveSpace V) st
for q3, r3 being Element of (ProjectiveSpace V) holds
( not r1,r2,r3 are_collinear or not q1,q2,q3 are_collinear or not p,r3,q3 are_collinear ) ) or ex CS being CollProjectiveSpace st
( CS = ProjectiveSpace V & CS is at_most-3-dimensional ) )
defpred S1[ Element of (ProjectiveSpace V), Element of (ProjectiveSpace V), Element of (ProjectiveSpace V)] means for y1, y2 being Element of (ProjectiveSpace V) ex x2, x1 being Element of (ProjectiveSpace V) st
( y1,y2,x1 are_collinear & $2,$3,x2 are_collinear & $1,x1,x2 are_collinear );
A3:
for p, q1, q2 being Element of (ProjectiveSpace V) st q1,q2,p are_collinear holds
S1[p,q1,q2]
proof
let p,
q1,
q2 be
Element of
(ProjectiveSpace V);
( q1,q2,p are_collinear implies S1[p,q1,q2] )
assume A4:
q1,
q2,
p are_collinear
;
S1[p,q1,q2]
now for y1, y2 being Element of (ProjectiveSpace V) ex x2, x1 being Element of (ProjectiveSpace V) st
( y1,y2,x1 are_collinear & q1,q2,x2 are_collinear & p,x1,x2 are_collinear )let y1,
y2 be
Element of
(ProjectiveSpace V);
ex x2, x1 being Element of (ProjectiveSpace V) st
( y1,y2,x1 are_collinear & q1,q2,x2 are_collinear & p,x1,x2 are_collinear )
(
y1,
y2,
y2 are_collinear &
p,
y2,
p are_collinear )
by Def7;
hence
ex
x2,
x1 being
Element of
(ProjectiveSpace V) st
(
y1,
y2,
x1 are_collinear &
q1,
q2,
x2 are_collinear &
p,
x1,
x2 are_collinear )
by A4;
verum end;
hence
S1[
p,
q1,
q2]
;
verum
end;
A5:
for q, q1, q2, p1, p2, x being Element of (ProjectiveSpace V) st S1[q,q1,q2] & not q1,q2,q are_collinear & q1,q2,x are_collinear & not p1,p2,q are_collinear & p1,p2,x are_collinear holds
S1[q,p1,p2]
proof
let q,
q1,
q2,
p1,
p2,
x be
Element of
(ProjectiveSpace V);
( S1[q,q1,q2] & not q1,q2,q are_collinear & q1,q2,x are_collinear & not p1,p2,q are_collinear & p1,p2,x are_collinear implies S1[q,p1,p2] )
assume that A6:
S1[
q,
q1,
q2]
and A7:
not
q1,
q2,
q are_collinear
and A8:
q1,
q2,
x are_collinear
and A9:
not
p1,
p2,
q are_collinear
and A10:
p1,
p2,
x are_collinear
;
S1[q,p1,p2]
A11:
q1 <> q2
by A7, Def7;
A12:
p1 <> p2
by A9, Def7;
now for y1, y2 being Element of (ProjectiveSpace V) ex z2, z1 being Element of (ProjectiveSpace V) st
( y1,y2,z1 are_collinear & p1,p2,z2 are_collinear & q,z1,z2 are_collinear )let y1,
y2 be
Element of
(ProjectiveSpace V);
ex z2, z1 being Element of (ProjectiveSpace V) st
( y1,y2,z1 are_collinear & p1,p2,z2 are_collinear & q,z1,z2 are_collinear )A13:
now ( y1 <> y2 implies ex z2, z1 being Element of (ProjectiveSpace V) st
( y1,y2,z1 are_collinear & p1,p2,z2 are_collinear & q,z1,z2 are_collinear ) )
ex
a being
Element of
(ProjectiveSpace V) st
(
p1,
p2,
a are_collinear &
x <> a )
then consider x1 being
Element of
(ProjectiveSpace V) such that A17:
p1,
p2,
x1 are_collinear
and A18:
x <> x1
;
consider b,
b9 being
Element of
(ProjectiveSpace V) such that A19:
y1,
y2,
b9 are_collinear
and A20:
q1,
q2,
b are_collinear
and A21:
q,
b9,
b are_collinear
by A6;
assume A22:
y1 <> y2
;
ex z2, z1 being Element of (ProjectiveSpace V) st
( y1,y2,z1 are_collinear & p1,p2,z2 are_collinear & q,z1,z2 are_collinear )
ex
a being
Element of
(ProjectiveSpace V) st
(
y1,
y2,
a are_collinear &
b9 <> a )
then consider x3 being
Element of
(ProjectiveSpace V) such that A26:
b9 <> x3
and A27:
y1,
y2,
x3 are_collinear
;
consider d,
d9 being
Element of
(ProjectiveSpace V) such that A28:
x1,
x3,
d9 are_collinear
and A29:
q1,
q2,
d are_collinear
and A30:
q,
d9,
d are_collinear
by A6;
A31:
b,
d,
x are_collinear
by A8, A11, A20, A29, Def8;
A32:
now ( b <> d implies ex z2, z1 being Element of (ProjectiveSpace V) st
( y1,y2,z1 are_collinear & p1,p2,z2 are_collinear & q,z1,z2 are_collinear ) )assume A33:
b <> d
;
ex z2, z1 being Element of (ProjectiveSpace V) st
( y1,y2,z1 are_collinear & p1,p2,z2 are_collinear & q,z1,z2 are_collinear )
not
q,
b,
d are_collinear
proof
q1,
q2,
q2 are_collinear
by Def7;
then A34:
b,
d,
q2 are_collinear
by A11, A20, A29, Def8;
assume
q,
b,
d are_collinear
;
contradiction
then A35:
b,
d,
q are_collinear
by Th24;
q1,
q2,
q1 are_collinear
by Def7;
then
b,
d,
q1 are_collinear
by A11, A20, A29, Def8;
hence
contradiction
by A7, A33, A35, A34, Def8;
verum
end; then consider o being
Element of
(ProjectiveSpace V) such that A36:
b9,
d9,
o are_collinear
and A37:
q,
x,
o are_collinear
by A21, A30, A31, Lm44;
A38:
o,
x,
q are_collinear
by A37, Th24;
d9,
x3,
x1 are_collinear
by A28, Th24;
then consider z1 being
Element of
(ProjectiveSpace V) such that A39:
b9,
x3,
z1 are_collinear
and A40:
o,
x1,
z1 are_collinear
by A36, Def9;
x1,
o,
z1 are_collinear
by A40, Th24;
then consider z2 being
Element of
(ProjectiveSpace V) such that A41:
x1,
x,
z2 are_collinear
and A42:
z1,
q,
z2 are_collinear
by A38, Def9;
A43:
q,
z1,
z2 are_collinear
by A42, Th24;
p1,
p2,
p2 are_collinear
by Def7;
then A44:
x1,
x,
p2 are_collinear
by A10, A12, A17, Def8;
y1,
y2,
y2 are_collinear
by Def7;
then A45:
b9,
x3,
y2 are_collinear
by A22, A19, A27, Def8;
p1,
p2,
p1 are_collinear
by Def7;
then
x1,
x,
p1 are_collinear
by A10, A12, A17, Def8;
then A46:
p1,
p2,
z2 are_collinear
by A18, A41, A44, Def8;
y1,
y2,
y1 are_collinear
by Def7;
then
b9,
x3,
y1 are_collinear
by A22, A19, A27, Def8;
then
y1,
y2,
z1 are_collinear
by A26, A39, A45, Def8;
hence
ex
z2,
z1 being
Element of
(ProjectiveSpace V) st
(
y1,
y2,
z1 are_collinear &
p1,
p2,
z2 are_collinear &
q,
z1,
z2 are_collinear )
by A46, A43;
verum end; now ( b = d implies ex z2, z1 being Element of (ProjectiveSpace V) st
( y1,y2,z1 are_collinear & p1,p2,z2 are_collinear & q,z1,z2 are_collinear ) )assume
b = d
;
ex z2, z1 being Element of (ProjectiveSpace V) st
( y1,y2,z1 are_collinear & p1,p2,z2 are_collinear & q,z1,z2 are_collinear )then A47:
b,
q,
d9 are_collinear
by A30, Th24;
y1,
y2,
y2 are_collinear
by Def7;
then A48:
b9,
x3,
y2 are_collinear
by A22, A19, A27, Def8;
A49:
d9,
x3,
x1 are_collinear
by A28, Th24;
(
b,
q,
b9 are_collinear &
b,
q,
q are_collinear )
by A21, Def7, Th24;
then
b9,
d9,
q are_collinear
by A7, A20, A47, Def8;
then consider z1 being
Element of
(ProjectiveSpace V) such that A50:
b9,
x3,
z1 are_collinear
and A51:
q,
x1,
z1 are_collinear
by A49, Def9;
A52:
q,
z1,
x1 are_collinear
by A51, Th24;
y1,
y2,
y1 are_collinear
by Def7;
then
b9,
x3,
y1 are_collinear
by A22, A19, A27, Def8;
then
y1,
y2,
z1 are_collinear
by A26, A50, A48, Def8;
hence
ex
z2,
z1 being
Element of
(ProjectiveSpace V) st
(
y1,
y2,
z1 are_collinear &
p1,
p2,
z2 are_collinear &
q,
z1,
z2 are_collinear )
by A17, A52;
verum end; hence
ex
z2,
z1 being
Element of
(ProjectiveSpace V) st
(
y1,
y2,
z1 are_collinear &
p1,
p2,
z2 are_collinear &
q,
z1,
z2 are_collinear )
by A32;
verum now ( y1 = y2 implies ex z2, z1 being Element of (ProjectiveSpace V) st
( y1,y2,z1 are_collinear & p1,p2,z2 are_collinear & q,z1,z2 are_collinear ) )assume
y1 = y2
;
ex z2, z1 being Element of (ProjectiveSpace V) st
( y1,y2,z1 are_collinear & p1,p2,z2 are_collinear & q,z1,z2 are_collinear )then A53:
y1,
y2,
q are_collinear
by Def7;
(
p1,
p2,
p1 are_collinear &
q,
q,
p1 are_collinear )
by Def7;
hence
ex
z2,
z1 being
Element of
(ProjectiveSpace V) st
(
y1,
y2,
z1 are_collinear &
p1,
p2,
z2 are_collinear &
q,
z1,
z2 are_collinear )
by A53;
verum end; hence
ex
z2,
z1 being
Element of
(ProjectiveSpace V) st
(
y1,
y2,
z1 are_collinear &
p1,
p2,
z2 are_collinear &
q,
z1,
z2 are_collinear )
by A13;
verum end;
hence
S1[
q,
p1,
p2]
;
verum
end;
A54:
for q1, q2, p1, p2, q being Element of (ProjectiveSpace V) st not q1,q2,q are_collinear & not p1,p2,q are_collinear & ( for x being Element of (ProjectiveSpace V) holds
( not q1,q2,x are_collinear or not p1,p2,x are_collinear ) ) holds
ex q3, p3 being Element of (ProjectiveSpace V) st
( p1,p2,p3 are_collinear & q1,q2,q3 are_collinear & not q3,p3,q are_collinear )
proof
let q1,
q2,
p1,
p2,
q be
Element of
(ProjectiveSpace V);
( not q1,q2,q are_collinear & not p1,p2,q are_collinear & ( for x being Element of (ProjectiveSpace V) holds
( not q1,q2,x are_collinear or not p1,p2,x are_collinear ) ) implies ex q3, p3 being Element of (ProjectiveSpace V) st
( p1,p2,p3 are_collinear & q1,q2,q3 are_collinear & not q3,p3,q are_collinear ) )
assume that A55:
not
q1,
q2,
q are_collinear
and A56:
not
p1,
p2,
q are_collinear
and
for
x being
Element of
(ProjectiveSpace V) holds
( not
q1,
q2,
x are_collinear or not
p1,
p2,
x are_collinear )
;
ex q3, p3 being Element of (ProjectiveSpace V) st
( p1,p2,p3 are_collinear & q1,q2,q3 are_collinear & not q3,p3,q are_collinear )
A57:
q <> q1
by A55, Def7;
A58:
( not
q1,
p1,
q are_collinear or not
q1,
p2,
q are_collinear )
proof
assume
(
q1,
p1,
q are_collinear &
q1,
p2,
q are_collinear )
;
contradiction
then A59:
(
q,
q1,
p1 are_collinear &
q,
q1,
p2 are_collinear )
by Th24;
q,
q1,
q are_collinear
by Def7;
hence
contradiction
by A56, A57, A59, Def8;
verum
end;
A60:
p1,
p2,
p2 are_collinear
by Def7;
(
q1,
q2,
q1 are_collinear &
p1,
p2,
p1 are_collinear )
by Def7;
hence
ex
q3,
p3 being
Element of
(ProjectiveSpace V) st
(
p1,
p2,
p3 are_collinear &
q1,
q2,
q3 are_collinear & not
q3,
p3,
q are_collinear )
by A60, A58;
verum
end;
A61:
for q, q1, q2, p1, p2 being Element of (ProjectiveSpace V) st S1[q,q1,q2] & not q1,q2,q are_collinear & not p1,p2,q are_collinear & ( for x being Element of (ProjectiveSpace V) holds
( not q1,q2,x are_collinear or not p1,p2,x are_collinear ) ) holds
S1[q,p1,p2]
proof
let q,
q1,
q2,
p1,
p2 be
Element of
(ProjectiveSpace V);
( S1[q,q1,q2] & not q1,q2,q are_collinear & not p1,p2,q are_collinear & ( for x being Element of (ProjectiveSpace V) holds
( not q1,q2,x are_collinear or not p1,p2,x are_collinear ) ) implies S1[q,p1,p2] )
assume that A62:
S1[
q,
q1,
q2]
and A63:
not
q1,
q2,
q are_collinear
and A64:
not
p1,
p2,
q are_collinear
and A65:
for
x being
Element of
(ProjectiveSpace V) holds
( not
q1,
q2,
x are_collinear or not
p1,
p2,
x are_collinear )
;
S1[q,p1,p2]
consider q3,
p3 being
Element of
(ProjectiveSpace V) such that A66:
p1,
p2,
p3 are_collinear
and A67:
q1,
q2,
q3 are_collinear
and A68:
not
q3,
p3,
q are_collinear
by A54, A63, A64, A65;
q3,
p3,
q3 are_collinear
by Def7;
then A69:
S1[
q,
q3,
p3]
by A5, A62, A63, A67, A68;
q3,
p3,
p3 are_collinear
by Def7;
hence
S1[
q,
p1,
p2]
by A5, A64, A66, A68, A69;
verum
end;
A70:
for q, q1, q2 being Element of (ProjectiveSpace V) st S1[q,q1,q2] & not q1,q2,q are_collinear holds
for p1, p2 being Element of (ProjectiveSpace V) holds S1[q,p1,p2]
proof
let q,
q1,
q2 be
Element of
(ProjectiveSpace V);
( S1[q,q1,q2] & not q1,q2,q are_collinear implies for p1, p2 being Element of (ProjectiveSpace V) holds S1[q,p1,p2] )
assume A71:
(
S1[
q,
q1,
q2] & not
q1,
q2,
q are_collinear )
;
for p1, p2 being Element of (ProjectiveSpace V) holds S1[q,p1,p2]
let p1,
p2 be
Element of
(ProjectiveSpace V);
S1[q,p1,p2]
A72:
( not
p1,
p2,
q are_collinear & ( for
x being
Element of
(ProjectiveSpace V) holds
( not
q1,
q2,
x are_collinear or not
p1,
p2,
x are_collinear ) ) implies
S1[
q,
p1,
p2] )
by A61, A71;
( not
p1,
p2,
q are_collinear & ex
x being
Element of
(ProjectiveSpace V) st
(
q1,
q2,
x are_collinear &
p1,
p2,
x are_collinear ) implies
S1[
q,
p1,
p2] )
by A5, A71;
hence
S1[
q,
p1,
p2]
by A3, A72;
verum
end;
reconsider CS = ProjectiveSpace V as CollProjectiveSpace by A1, A2, Def10;
given p, q1, q2 being Element of (ProjectiveSpace V) such that A73:
not p,q1,q2 are_collinear
and
A74:
for r1, r2 being Element of (ProjectiveSpace V) ex q3, r3 being Element of (ProjectiveSpace V) st
( r1,r2,r3 are_collinear & q1,q2,q3 are_collinear & p,r3,q3 are_collinear )
; ex CS being CollProjectiveSpace st
( CS = ProjectiveSpace V & CS is at_most-3-dimensional )
take
CS
; ( CS = ProjectiveSpace V & CS is at_most-3-dimensional )
A75:
for q, q1, q2, x, q3 being Element of (ProjectiveSpace V) st S1[q,q1,q2] & not q1,q2,q are_collinear & q1,q2,x are_collinear & q,q3,x are_collinear holds
S1[q3,q1,q2]
proof
let q,
q1,
q2,
x,
q3 be
Element of
(ProjectiveSpace V);
( S1[q,q1,q2] & not q1,q2,q are_collinear & q1,q2,x are_collinear & q,q3,x are_collinear implies S1[q3,q1,q2] )
assume that A76:
S1[
q,
q1,
q2]
and A77:
not
q1,
q2,
q are_collinear
and A78:
q1,
q2,
x are_collinear
and A79:
q,
q3,
x are_collinear
;
S1[q3,q1,q2]
now for y1, y2 being Element of (ProjectiveSpace V) ex x2, x1 being Element of (ProjectiveSpace V) st
( y1,y2,x1 are_collinear & q1,q2,x2 are_collinear & q3,x1,x2 are_collinear )let y1,
y2 be
Element of
(ProjectiveSpace V);
ex x2, x1 being Element of (ProjectiveSpace V) st
( y1,y2,x1 are_collinear & q1,q2,x2 are_collinear & q3,x1,x2 are_collinear )consider z2,
z1 being
Element of
(ProjectiveSpace V) such that A80:
y1,
y2,
z1 are_collinear
and A81:
q1,
q2,
z2 are_collinear
and A82:
q,
z1,
z2 are_collinear
by A76;
A83:
now ( x <> z2 implies ex x2, x1 being Element of (ProjectiveSpace V) st
( y1,y2,x1 are_collinear & q1,q2,x2 are_collinear & q3,x1,x2 are_collinear ) )
q3,
q,
x are_collinear
by A79, Th24;
then consider x2 being
Element of
(ProjectiveSpace V) such that A84:
q3,
z1,
x2 are_collinear
and A85:
x,
z2,
x2 are_collinear
by A82, Def9;
A86:
q1 <> q2
by A77, Def7;
q1,
q2,
q2 are_collinear
by Def7;
then A87:
x,
z2,
q2 are_collinear
by A78, A81, A86, Def8;
q1,
q2,
q1 are_collinear
by Def7;
then A88:
x,
z2,
q1 are_collinear
by A78, A81, A86, Def8;
assume
x <> z2
;
ex x2, x1 being Element of (ProjectiveSpace V) st
( y1,y2,x1 are_collinear & q1,q2,x2 are_collinear & q3,x1,x2 are_collinear )then
q1,
q2,
x2 are_collinear
by A85, A88, A87, Def8;
hence
ex
x2,
x1 being
Element of
(ProjectiveSpace V) st
(
y1,
y2,
x1 are_collinear &
q1,
q2,
x2 are_collinear &
q3,
x1,
x2 are_collinear )
by A80, A84;
verum end; now ( x = z2 implies ex x2, x1 being Element of (ProjectiveSpace V) st
( y1,y2,x1 are_collinear & q1,q2,x2 are_collinear & q3,x1,x2 are_collinear ) )A89:
(
q,
x,
q3 are_collinear &
q,
x,
x are_collinear )
by A79, Def7, Th24;
assume A90:
x = z2
;
ex x2, x1 being Element of (ProjectiveSpace V) st
( y1,y2,x1 are_collinear & q1,q2,x2 are_collinear & q3,x1,x2 are_collinear )then
q,
x,
z1 are_collinear
by A82, Th24;
then
q3,
z1,
z2 are_collinear
by A77, A78, A90, A89, Def8;
hence
ex
x2,
x1 being
Element of
(ProjectiveSpace V) st
(
y1,
y2,
x1 are_collinear &
q1,
q2,
x2 are_collinear &
q3,
x1,
x2 are_collinear )
by A80, A81;
verum end; hence
ex
x2,
x1 being
Element of
(ProjectiveSpace V) st
(
y1,
y2,
x1 are_collinear &
q1,
q2,
x2 are_collinear &
q3,
x1,
x2 are_collinear )
by A83;
verum end;
hence
S1[
q3,
q1,
q2]
;
verum
end;
A91:
for q, p being Element of (ProjectiveSpace V) st ( for q1, q2 being Element of (ProjectiveSpace V) holds S1[q,q1,q2] ) holds
ex p1, p2 being Element of (ProjectiveSpace V) st
( S1[p,p1,p2] & not p1,p2,p are_collinear )
proof
let q,
p be
Element of
(ProjectiveSpace V);
( ( for q1, q2 being Element of (ProjectiveSpace V) holds S1[q,q1,q2] ) implies ex p1, p2 being Element of (ProjectiveSpace V) st
( S1[p,p1,p2] & not p1,p2,p are_collinear ) )
assume A92:
for
q1,
q2 being
Element of
(ProjectiveSpace V) holds
S1[
q,
q1,
q2]
;
ex p1, p2 being Element of (ProjectiveSpace V) st
( S1[p,p1,p2] & not p1,p2,p are_collinear )
consider x1 being
Element of
(ProjectiveSpace V) such that A93:
p <> x1
and A94:
q <> x1
and A95:
p,
q,
x1 are_collinear
by A2;
consider x2 being
Element of
(ProjectiveSpace V) such that A96:
not
p,
x1,
x2 are_collinear
by A1, A93, COLLSP:12;
A97:
not
x1,
x2,
q are_collinear
proof
assume
x1,
x2,
q are_collinear
;
contradiction
then A98:
q,
x1,
x2 are_collinear
by Th24;
(
q,
x1,
x1 are_collinear &
q,
x1,
p are_collinear )
by A95, Def7, Th24;
hence
contradiction
by A94, A96, A98, Def8;
verum
end;
A99:
x1,
x2,
x1 are_collinear
by Def7;
A100:
not
x1,
x2,
p are_collinear
by A96, Th24;
A101:
S1[
q,
x1,
x2]
by A92;
q,
p,
x1 are_collinear
by A95, Th24;
then
S1[
p,
x1,
x2]
by A75, A97, A99, A101;
hence
ex
p1,
p2 being
Element of
(ProjectiveSpace V) st
(
S1[
p,
p1,
p2] & not
p1,
p2,
p are_collinear )
by A100;
verum
end;
A102:
for x, y1, z being Element of (ProjectiveSpace V) holds S1[x,y1,z]
proof
let x,
y1,
z be
Element of
(ProjectiveSpace V);
S1[x,y1,z]
not
q1,
q2,
p are_collinear
by A73, Th24;
then
for
p1,
p2 being
Element of
(ProjectiveSpace V) holds
S1[
p,
p1,
p2]
by A74, A70;
then
ex
r1,
r2 being
Element of
(ProjectiveSpace V) st
(
S1[
x,
r1,
r2] & not
r1,
r2,
x are_collinear )
by A91;
hence
S1[
x,
y1,
z]
by A70;
verum
end;
for p4, p1, q, q4, r2 being Element of (ProjectiveSpace V) ex r, r1 being Element of (ProjectiveSpace V) st
( p4,q,r are_collinear & p1,q4,r1 are_collinear & r2,r,r1 are_collinear )
proof
let p4,
p1,
q,
q4,
r2 be
Element of
(ProjectiveSpace V);
ex r, r1 being Element of (ProjectiveSpace V) st
( p4,q,r are_collinear & p1,q4,r1 are_collinear & r2,r,r1 are_collinear )
ex
r1,
r being
Element of
(ProjectiveSpace V) st
(
p4,
q,
r are_collinear &
p1,
q4,
r1 are_collinear &
r2,
r,
r1 are_collinear )
by A102;
hence
ex
r,
r1 being
Element of
(ProjectiveSpace V) st
(
p4,
q,
r are_collinear &
p1,
q4,
r1 are_collinear &
r2,
r,
r1 are_collinear )
;
verum
end;
hence
( CS = ProjectiveSpace V & CS is at_most-3-dimensional )
; verum