let V be non trivial RealLinearSpace; :: thesis: ( 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 ) ; :: according to ANPROJ_2:def 10 :: thesis: ( 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 S₁[ 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
S₁[p,q1,q2]

proof

let p, q1, q2 be Element of (ProjectiveSpace V); :: thesis: ( q1,q2,p are_collinear implies S₁[p,q1,q2] )
assume A4: q1,q2,p are_collinear ; :: thesis: S₁[p,q1,q2]

now :: thesis: 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); :: thesis: 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; :: thesis: verum

end;

hence S₁[p,q1,q2] ; :: thesis: verum

end;

A5: for q, q1, q2, p1, p2, x being Element of (ProjectiveSpace V) st S₁[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
S₁[q,p1,p2]

proof

let q, q1, q2, p1, p2, x be Element of (ProjectiveSpace V); :: thesis: ( S₁[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 S₁[q,p1,p2] )
assume that
A6: S₁[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 ; :: thesis: S₁[q,p1,p2]
A11: q1 <> q2 by A7, Def7;
A12: p1 <> p2 by A9, Def7;

now :: thesis: 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); :: thesis: 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 :: thesis: ( 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 )

proof

A14: now :: thesis: ( x <> p2 implies ex p2, a being Element of (ProjectiveSpace V) st
( p1,p2,a are_collinear & x <> a ) )

assume A15: x <> p2 ; :: thesis: ex p2, a being Element of (ProjectiveSpace V) st
( p1,p2,a are_collinear & x <> a )
take p2 = p2; :: thesis: ex a being Element of (ProjectiveSpace V) st
( p1,p2,a are_collinear & x <> a )
p1,p2,p2 are_collinear by Def7;
hence ex a being Element of (ProjectiveSpace V) st
( p1,p2,a are_collinear & x <> a ) by A15; :: thesis: verum

end;

now :: thesis: ( x <> p1 implies ex p1, a being Element of (ProjectiveSpace V) st
( p1,p2,a are_collinear & x <> a ) )

assume A16: x <> p1 ; :: thesis: ex p1, a being Element of (ProjectiveSpace V) st
( p1,p2,a are_collinear & x <> a )
take p1 = p1; :: thesis: ex a being Element of (ProjectiveSpace V) st
( p1,p2,a are_collinear & x <> a )
p1,p2,p1 are_collinear by Def7;
hence ex a being Element of (ProjectiveSpace V) st
( p1,p2,a are_collinear & x <> a ) by A16; :: thesis: verum

end;

hence ex a being Element of (ProjectiveSpace V) st
( p1,p2,a are_collinear & x <> a ) by A9, A14, Def7; :: thesis: verum

end;

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 ; :: thesis: 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 )

proof

A23: now :: thesis: ( b9 <> y2 implies ex y2, a being Element of (ProjectiveSpace V) st
( y1,y2,a are_collinear & b9 <> a ) )

assume A24: b9 <> y2 ; :: thesis: ex y2, a being Element of (ProjectiveSpace V) st
( y1,y2,a are_collinear & b9 <> a )
take y2 = y2; :: thesis: ex a being Element of (ProjectiveSpace V) st
( y1,y2,a are_collinear & b9 <> a )
y1,y2,y2 are_collinear by Def7;
hence ex a being Element of (ProjectiveSpace V) st
( y1,y2,a are_collinear & b9 <> a ) by A24; :: thesis: verum

end;

now :: thesis: ( b9 <> y1 implies ex y1, a being Element of (ProjectiveSpace V) st
( y1,y2,a are_collinear & b9 <> a ) )

assume A25: b9 <> y1 ; :: thesis: ex y1, a being Element of (ProjectiveSpace V) st
( y1,y2,a are_collinear & b9 <> a )
take y1 = y1; :: thesis: ex a being Element of (ProjectiveSpace V) st
( y1,y2,a are_collinear & b9 <> a )
y1,y2,y1 are_collinear by Def7;
hence ex a being Element of (ProjectiveSpace V) st
( y1,y2,a are_collinear & b9 <> a ) by A25; :: thesis: verum

end;

hence ex a being Element of (ProjectiveSpace V) st
( y1,y2,a are_collinear & b9 <> a ) by A22, A23; :: thesis: verum

end;

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 :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: verum

end;

now :: thesis: ( 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 ; :: thesis: 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; :: thesis: 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; :: thesis: verum

end;

now :: thesis: ( 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 ; :: thesis: 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; :: thesis: 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; :: thesis: verum

end;

hence S₁[q,p1,p2] ; :: thesis: 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); :: thesis: ( 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 ) ; :: thesis: 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 ) ; :: thesis: 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; :: thesis: 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; :: thesis: verum

end;

A61: for q, q1, q2, p1, p2 being Element of (ProjectiveSpace V) st S₁[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
S₁[q,p1,p2]

proof

let q, q1, q2, p1, p2 be Element of (ProjectiveSpace V); :: thesis: ( S₁[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 S₁[q,p1,p2] )
assume that
A62: S₁[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 ) ; :: thesis: S₁[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: S₁[q,q3,p3] by A5, A62, A63, A67, A68;
q3,p3,p3 are_collinear by Def7;
hence S₁[q,p1,p2] by A5, A64, A66, A68, A69; :: thesis: verum

end;

A70: for q, q1, q2 being Element of (ProjectiveSpace V) st S₁[q,q1,q2] & not q1,q2,q are_collinear holds
for p1, p2 being Element of (ProjectiveSpace V) holds S₁[q,p1,p2]

proof

let q, q1, q2 be Element of (ProjectiveSpace V); :: thesis: ( S₁[q,q1,q2] & not q1,q2,q are_collinear implies for p1, p2 being Element of (ProjectiveSpace V) holds S₁[q,p1,p2] )
assume A71: ( S₁[q,q1,q2] & not q1,q2,q are_collinear ) ; :: thesis: for p1, p2 being Element of (ProjectiveSpace V) holds S₁[q,p1,p2]
let p1, p2 be Element of (ProjectiveSpace V); :: thesis: S₁[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 S₁[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 S₁[q,p1,p2] ) by A5, A71;
hence S₁[q,p1,p2] by A3, A72; :: thesis: 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 ) ; :: thesis: ex CS being CollProjectiveSpace st
( CS = ProjectiveSpace V & CS is at_most-3-dimensional )
take CS ; :: thesis: ( CS = ProjectiveSpace V & CS is at_most-3-dimensional )
A75: for q, q1, q2, x, q3 being Element of (ProjectiveSpace V) st S₁[q,q1,q2] & not q1,q2,q are_collinear & q1,q2,x are_collinear & q,q3,x are_collinear holds
S₁[q3,q1,q2]

proof

let q, q1, q2, x, q3 be Element of (ProjectiveSpace V); :: thesis: ( S₁[q,q1,q2] & not q1,q2,q are_collinear & q1,q2,x are_collinear & q,q3,x are_collinear implies S₁[q3,q1,q2] )
assume that
A76: S₁[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 ; :: thesis: S₁[q3,q1,q2]

now :: thesis: 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); :: thesis: 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 :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum

end;

now :: thesis: ( 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 ; :: thesis: 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; :: thesis: 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; :: thesis: verum

end;

hence S₁[q3,q1,q2] ; :: thesis: verum

end;

A91: for q, p being Element of (ProjectiveSpace V) st ( for q1, q2 being Element of (ProjectiveSpace V) holds S₁[q,q1,q2] ) holds
ex p1, p2 being Element of (ProjectiveSpace V) st
( S₁[p,p1,p2] & not p1,p2,p are_collinear )

proof

let q, p be Element of (ProjectiveSpace V); :: thesis: ( ( for q1, q2 being Element of (ProjectiveSpace V) holds S₁[q,q1,q2] ) implies ex p1, p2 being Element of (ProjectiveSpace V) st
( S₁[p,p1,p2] & not p1,p2,p are_collinear ) )
assume A92: for q1, q2 being Element of (ProjectiveSpace V) holds S₁[q,q1,q2] ; :: thesis: ex p1, p2 being Element of (ProjectiveSpace V) st
( S₁[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 ; :: thesis: 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; :: thesis: verum

end;

A99: x1,x2,x1 are_collinear by Def7;
A100: not x1,x2,p are_collinear by A96, Th24;
A101: S₁[q,x1,x2] by A92;
q,p,x1 are_collinear by A95, Th24;
then S₁[p,x1,x2] by A75, A97, A99, A101;
hence ex p1, p2 being Element of (ProjectiveSpace V) st
( S₁[p,p1,p2] & not p1,p2,p are_collinear ) by A100; :: thesis: verum

end;

A102: for x, y1, z being Element of (ProjectiveSpace V) holds S₁[x,y1,z]

proof

let x, y1, z be Element of (ProjectiveSpace V); :: thesis: S₁[x,y1,z]
not q1,q2,p are_collinear by A73, Th24;
then for p1, p2 being Element of (ProjectiveSpace V) holds S₁[p,p1,p2] by A74, A70;
then ex r1, r2 being Element of (ProjectiveSpace V) st
( S₁[x,r1,r2] & not r1,r2,x are_collinear ) by A91;
hence S₁[x,y1,z] by A70; :: thesis: 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); :: thesis: 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 ) ; :: thesis: verum

end;

hence ( CS = ProjectiveSpace V & CS is at_most-3-dimensional ) ; :: thesis: verum