let V be non trivial RealLinearSpace; :: thesis: ( ProjectiveSpace V is proper & ProjectiveSpace V is at_least_3rank & ex p, q1, q2 being Element of () st
( not p,q1,q2 are_collinear & ( for r1, r2 being Element of () ex q3, r3 being Element of () 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 () ex r being Element of () st
( p <> r & q <> r & p,q,r are_collinear ) ; :: according to ANPROJ_2:def 10 :: thesis: ( for p, q1, q2 being Element of () holds
( p,q1,q2 are_collinear or ex r1, r2 being Element of () st
for q3, r3 being Element of () 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 (), Element of (), Element of ()] means for y1, y2 being Element of () ex x2, x1 being Element of () st
( y1,y2,x1 are_collinear & \$2,\$3,x2 are_collinear & \$1,x1,x2 are_collinear );
A3: for p, q1, q2 being Element of () st q1,q2,p are_collinear holds
S1[p,q1,q2]
proof
let p, q1, q2 be Element of (); :: thesis: ( q1,q2,p are_collinear implies S1[p,q1,q2] )
assume A4: q1,q2,p are_collinear ; :: thesis: S1[p,q1,q2]
now :: thesis: for y1, y2 being Element of () ex x2, x1 being Element of () st
( y1,y2,x1 are_collinear & q1,q2,x2 are_collinear & p,x1,x2 are_collinear )
let y1, y2 be Element of (); :: thesis: ex x2, x1 being Element of () 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 () st
( y1,y2,x1 are_collinear & q1,q2,x2 are_collinear & p,x1,x2 are_collinear ) by A4; :: thesis: verum
end;
hence S1[p,q1,q2] ; :: thesis: verum
end;
A5: for q, q1, q2, p1, p2, x being Element of () 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 (); :: thesis: ( 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 ; :: thesis: S1[q,p1,p2]
A11: q1 <> q2 by ;
A12: p1 <> p2 by ;
now :: thesis: for y1, y2 being Element of () ex z2, z1 being Element of () st
( y1,y2,z1 are_collinear & p1,p2,z2 are_collinear & q,z1,z2 are_collinear )
let y1, y2 be Element of (); :: thesis: ex z2, z1 being Element of () 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 () st
( y1,y2,z1 are_collinear & p1,p2,z2 are_collinear & q,z1,z2 are_collinear ) )
ex a being Element of () st
( p1,p2,a are_collinear & x <> a )
proof
A14: now :: thesis: ( x <> p2 implies ex p2, a being Element of () st
( p1,p2,a are_collinear & x <> a ) )
assume A15: x <> p2 ; :: thesis: ex p2, a being Element of () st
( p1,p2,a are_collinear & x <> a )

take p2 = p2; :: thesis: ex a being Element of () st
( p1,p2,a are_collinear & x <> a )

p1,p2,p2 are_collinear by Def7;
hence ex a being Element of () st
( p1,p2,a are_collinear & x <> a ) by A15; :: thesis: verum
end;
now :: thesis: ( x <> p1 implies ex p1, a being Element of () st
( p1,p2,a are_collinear & x <> a ) )
assume A16: x <> p1 ; :: thesis: ex p1, a being Element of () st
( p1,p2,a are_collinear & x <> a )

take p1 = p1; :: thesis: ex a being Element of () st
( p1,p2,a are_collinear & x <> a )

p1,p2,p1 are_collinear by Def7;
hence ex a being Element of () st
( p1,p2,a are_collinear & x <> a ) by A16; :: thesis: verum
end;
hence ex a being Element of () st
( p1,p2,a are_collinear & x <> a ) by ; :: thesis: verum
end;
then consider x1 being Element of () such that
A17: p1,p2,x1 are_collinear and
A18: x <> x1 ;
consider b, b9 being Element of () 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 () st
( y1,y2,z1 are_collinear & p1,p2,z2 are_collinear & q,z1,z2 are_collinear )

ex a being Element of () st
( y1,y2,a are_collinear & b9 <> a )
proof
A23: now :: thesis: ( b9 <> y2 implies ex y2, a being Element of () st
( y1,y2,a are_collinear & b9 <> a ) )
assume A24: b9 <> y2 ; :: thesis: ex y2, a being Element of () st
( y1,y2,a are_collinear & b9 <> a )

take y2 = y2; :: thesis: ex a being Element of () st
( y1,y2,a are_collinear & b9 <> a )

y1,y2,y2 are_collinear by Def7;
hence ex a being Element of () st
( y1,y2,a are_collinear & b9 <> a ) by A24; :: thesis: verum
end;
now :: thesis: ( b9 <> y1 implies ex y1, a being Element of () st
( y1,y2,a are_collinear & b9 <> a ) )
assume A25: b9 <> y1 ; :: thesis: ex y1, a being Element of () st
( y1,y2,a are_collinear & b9 <> a )

take y1 = y1; :: thesis: ex a being Element of () st
( y1,y2,a are_collinear & b9 <> a )

y1,y2,y1 are_collinear by Def7;
hence ex a being Element of () st
( y1,y2,a are_collinear & b9 <> a ) by A25; :: thesis: verum
end;
hence ex a being Element of () st
( y1,y2,a are_collinear & b9 <> a ) by ; :: thesis: verum
end;
then consider x3 being Element of () such that
A26: b9 <> x3 and
A27: y1,y2,x3 are_collinear ;
consider d, d9 being Element of () 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 () st
( y1,y2,z1 are_collinear & p1,p2,z2 are_collinear & q,z1,z2 are_collinear ) )
end;
now :: thesis: ( b = d implies ex z2, z1 being Element of () st
( y1,y2,z1 are_collinear & p1,p2,z2 are_collinear & q,z1,z2 are_collinear ) )
end;
hence ex z2, z1 being Element of () 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 () 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 () 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 () 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 () st
( y1,y2,z1 are_collinear & p1,p2,z2 are_collinear & q,z1,z2 are_collinear ) by A13; :: thesis: verum
end;
hence S1[q,p1,p2] ; :: thesis: verum
end;
A54: for q1, q2, p1, p2, q being Element of () st not q1,q2,q are_collinear & not p1,p2,q are_collinear & ( for x being Element of () holds
( not q1,q2,x are_collinear or not p1,p2,x are_collinear ) ) holds
ex q3, p3 being Element of () 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 (); :: thesis: ( not q1,q2,q are_collinear & not p1,p2,q are_collinear & ( for x being Element of () holds
( not q1,q2,x are_collinear or not p1,p2,x are_collinear ) ) implies ex q3, p3 being Element of () 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 () holds
( not q1,q2,x are_collinear or not p1,p2,x are_collinear ) ; :: thesis: ex q3, p3 being Element of () st
( p1,p2,p3 are_collinear & q1,q2,q3 are_collinear & not q3,p3,q are_collinear )

A57: q <> q1 by ;
A58: ( not q1,p1,q are_collinear or not q1,p2,q are_collinear )
proof 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 () st
( p1,p2,p3 are_collinear & q1,q2,q3 are_collinear & not q3,p3,q are_collinear ) by ; :: thesis: verum
end;
A61: for q, q1, q2, p1, p2 being Element of () st S1[q,q1,q2] & not q1,q2,q are_collinear & not p1,p2,q are_collinear & ( for x being Element of () 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 (); :: thesis: ( S1[q,q1,q2] & not q1,q2,q are_collinear & not p1,p2,q are_collinear & ( for x being Element of () 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 () holds
( not q1,q2,x are_collinear or not p1,p2,x are_collinear ) ; :: thesis: S1[q,p1,p2]
consider q3, p3 being Element of () 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; :: thesis: verum
end;
A70: for q, q1, q2 being Element of () st S1[q,q1,q2] & not q1,q2,q are_collinear holds
for p1, p2 being Element of () holds S1[q,p1,p2]
proof
let q, q1, q2 be Element of (); :: thesis: ( S1[q,q1,q2] & not q1,q2,q are_collinear implies for p1, p2 being Element of () holds S1[q,p1,p2] )
assume A71: ( S1[q,q1,q2] & not q1,q2,q are_collinear ) ; :: thesis: for p1, p2 being Element of () holds S1[q,p1,p2]
let p1, p2 be Element of (); :: thesis: S1[q,p1,p2]
A72: ( not p1,p2,q are_collinear & ( for x being Element of () holds
( not q1,q2,x are_collinear or not p1,p2,x are_collinear ) ) implies S1[q,p1,p2] ) by ;
( not p1,p2,q are_collinear & ex x being Element of () st
( q1,q2,x are_collinear & p1,p2,x are_collinear ) implies S1[q,p1,p2] ) by ;
hence S1[q,p1,p2] by A3, A72; :: thesis: verum
end;
reconsider CS = ProjectiveSpace V as CollProjectiveSpace by ;
given p, q1, q2 being Element of () such that A73: not p,q1,q2 are_collinear and
A74: for r1, r2 being Element of () ex q3, r3 being Element of () 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 () 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 (); :: thesis: ( 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 ; :: thesis: S1[q3,q1,q2]
now :: thesis: for y1, y2 being Element of () ex x2, x1 being Element of () st
( y1,y2,x1 are_collinear & q1,q2,x2 are_collinear & q3,x1,x2 are_collinear )
let y1, y2 be Element of (); :: thesis: ex x2, x1 being Element of () st
( y1,y2,x1 are_collinear & q1,q2,x2 are_collinear & q3,x1,x2 are_collinear )

consider z2, z1 being Element of () 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 () st
( y1,y2,x1 are_collinear & q1,q2,x2 are_collinear & q3,x1,x2 are_collinear ) )
end;
now :: thesis: ( x = z2 implies ex x2, x1 being Element of () 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 ;
assume A90: x = z2 ; :: thesis: ex x2, x1 being Element of () st
( y1,y2,x1 are_collinear & q1,q2,x2 are_collinear & q3,x1,x2 are_collinear )

then q,x,z1 are_collinear by ;
then q3,z1,z2 are_collinear by A77, A78, A90, A89, Def8;
hence ex x2, x1 being Element of () st
( y1,y2,x1 are_collinear & q1,q2,x2 are_collinear & q3,x1,x2 are_collinear ) by ; :: thesis: verum
end;
hence ex x2, x1 being Element of () st
( y1,y2,x1 are_collinear & q1,q2,x2 are_collinear & q3,x1,x2 are_collinear ) by A83; :: thesis: verum
end;
hence S1[q3,q1,q2] ; :: thesis: verum
end;
A91: for q, p being Element of () st ( for q1, q2 being Element of () holds S1[q,q1,q2] ) holds
ex p1, p2 being Element of () st
( S1[p,p1,p2] & not p1,p2,p are_collinear )
proof
let q, p be Element of (); :: thesis: ( ( for q1, q2 being Element of () holds S1[q,q1,q2] ) implies ex p1, p2 being Element of () st
( S1[p,p1,p2] & not p1,p2,p are_collinear ) )

assume A92: for q1, q2 being Element of () holds S1[q,q1,q2] ; :: thesis: ex p1, p2 being Element of () st
( S1[p,p1,p2] & not p1,p2,p are_collinear )

consider x1 being Element of () such that
A93: p <> x1 and
A94: q <> x1 and
A95: p,q,x1 are_collinear by A2;
consider x2 being Element of () such that
A96: not p,x1,x2 are_collinear by ;
A97: not x1,x2,q are_collinear
proof end;
A99: x1,x2,x1 are_collinear by Def7;
A100: not x1,x2,p are_collinear by ;
A101: S1[q,x1,x2] by A92;
q,p,x1 are_collinear by ;
then S1[p,x1,x2] by A75, A97, A99, A101;
hence ex p1, p2 being Element of () st
( S1[p,p1,p2] & not p1,p2,p are_collinear ) by A100; :: thesis: verum
end;
A102: for x, y1, z being Element of () holds S1[x,y1,z]
proof
let x, y1, z be Element of (); :: thesis: S1[x,y1,z]
not q1,q2,p are_collinear by ;
then for p1, p2 being Element of () holds S1[p,p1,p2] by ;
then ex r1, r2 being Element of () st
( S1[x,r1,r2] & not r1,r2,x are_collinear ) by A91;
hence S1[x,y1,z] by A70; :: thesis: verum
end;
for p4, p1, q, q4, r2 being Element of () ex r, r1 being Element of () 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 (); :: thesis: ex r, r1 being Element of () st
( p4,q,r are_collinear & p1,q4,r1 are_collinear & r2,r,r1 are_collinear )

ex r1, r being Element of () 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 () 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