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 is_collinear & ( for r1, r2 being Element of (ProjectiveSpace V) ex q3, r3 being Element of (ProjectiveSpace V) st
( r1,r2,r3 is_collinear & q1,q2,q3 is_collinear & p,r3,q3 is_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 is_collinear ) ; :: according to ANPROJ_2:def 10 :: thesis: ( for p, q1, q2 being Element of (ProjectiveSpace V) holds
( p,q1,q2 is_collinear or ex r1, r2 being Element of (ProjectiveSpace V) st
for q3, r3 being Element of (ProjectiveSpace V) holds
( not r1,r2,r3 is_collinear or not q1,q2,q3 is_collinear or not p,r3,q3 is_collinear ) ) or ex CS being CollProjectiveSpace st
( CS = ProjectiveSpace V & CS is at_most-3-dimensional ) )
given p, q1, q2 being Element of (ProjectiveSpace V) such that A3: not p,q1,q2 is_collinear and
A4: for r1, r2 being Element of (ProjectiveSpace V) ex q3, r3 being Element of (ProjectiveSpace V) st
( r1,r2,r3 is_collinear & q1,q2,q3 is_collinear & p,r3,q3 is_collinear ) ; :: thesis: 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 is_collinear & $2,$3,x2 is_collinear & $1,x1,x2 is_collinear );
A5: for p, q1, q2 being Element of (ProjectiveSpace V) st q1,q2,p is_collinear holds
S₁[p,q1,q2]

proof

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

now

let y1, y2 be Element of (ProjectiveSpace V); :: thesis: ex x2, x1 being Element of (ProjectiveSpace V) st
( y1,y2,x1 is_collinear & q1,q2,x2 is_collinear & p,x1,x2 is_collinear )
( y1,y2,y2 is_collinear & q1,q2,p is_collinear & p,y2,p is_collinear ) by A6, Def7;
hence ex x2, x1 being Element of (ProjectiveSpace V) st
( y1,y2,x1 is_collinear & q1,q2,x2 is_collinear & p,x1,x2 is_collinear ) ; :: thesis: verum

end;

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

end;

A7: for q1, q2, p1, p2, q being Element of (ProjectiveSpace V) st not q1,q2,q is_collinear & not p1,p2,q is_collinear & ( for x being Element of (ProjectiveSpace V) holds
( not q1,q2,x is_collinear or not p1,p2,x is_collinear ) ) holds
ex q3, p3 being Element of (ProjectiveSpace V) st
( p1,p2,p3 is_collinear & q1,q2,q3 is_collinear & not q3,p3,q is_collinear )

proof

let q1, q2, p1, p2, q be Element of (ProjectiveSpace V); :: thesis: ( not q1,q2,q is_collinear & not p1,p2,q is_collinear & ( for x being Element of (ProjectiveSpace V) holds
( not q1,q2,x is_collinear or not p1,p2,x is_collinear ) ) implies ex q3, p3 being Element of (ProjectiveSpace V) st
( p1,p2,p3 is_collinear & q1,q2,q3 is_collinear & not q3,p3,q is_collinear ) )
assume that
A8: ( not q1,q2,q is_collinear & not p1,p2,q is_collinear ) and
for x being Element of (ProjectiveSpace V) holds
( not q1,q2,x is_collinear or not p1,p2,x is_collinear ) ; :: thesis: ex q3, p3 being Element of (ProjectiveSpace V) st
( p1,p2,p3 is_collinear & q1,q2,q3 is_collinear & not q3,p3,q is_collinear )
A9: ( q1,q2,q1 is_collinear & p1,p2,p1 is_collinear & p1,p2,p2 is_collinear ) by Def7;
A10: q <> q1 by A8, Def7;
( not q1,p1,q is_collinear or not q1,p2,q is_collinear )

proof

assume ( q1,p1,q is_collinear & q1,p2,q is_collinear ) ; :: thesis: contradiction
then A11: ( q,q1,p1 is_collinear & q,q1,p2 is_collinear ) by Th25;
q,q1,q is_collinear by Def7;
hence contradiction by A8, A10, A11, Def8; :: thesis: verum

end;

hence ex q3, p3 being Element of (ProjectiveSpace V) st
( p1,p2,p3 is_collinear & q1,q2,q3 is_collinear & not q3,p3,q is_collinear ) by A9; :: thesis: verum

end;

A12: for q, q1, q2, p1, p2, x being Element of (ProjectiveSpace V) st S₁[q,q1,q2] & not q1,q2,q is_collinear & q1,q2,x is_collinear & not p1,p2,q is_collinear & p1,p2,x is_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 is_collinear & q1,q2,x is_collinear & not p1,p2,q is_collinear & p1,p2,x is_collinear implies S₁[q,p1,p2] )
assume that
A13: S₁[q,q1,q2] and
A14: not q1,q2,q is_collinear and
A15: q1,q2,x is_collinear and
A16: not p1,p2,q is_collinear and
A17: p1,p2,x is_collinear ; :: thesis: S₁[q,p1,p2]
A18: ( q1 <> q2 & q1 <> q & q2 <> q ) by A14, Def7;
A19: ( p1 <> p2 & p1 <> q & p2 <> q ) by A16, Def7;

now

let y1, y2 be Element of (ProjectiveSpace V); :: thesis: ex z2, z1 being Element of (ProjectiveSpace V) st
( y1,y2,z1 is_collinear & p1,p2,z2 is_collinear & q,z1,z2 is_collinear )

A20: now

assume y1 = y2 ; :: thesis: ex z2, z1 being Element of (ProjectiveSpace V) st
( y1,y2,z1 is_collinear & p1,p2,z2 is_collinear & q,z1,z2 is_collinear )
then ( y1,y2,q is_collinear & p1,p2,p1 is_collinear & q,q,p1 is_collinear ) by Def7;
hence ex z2, z1 being Element of (ProjectiveSpace V) st
( y1,y2,z1 is_collinear & p1,p2,z2 is_collinear & q,z1,z2 is_collinear ) ; :: thesis: verum

end;

now

assume A21: y1 <> y2 ; :: thesis: ex z2, z1 being Element of (ProjectiveSpace V) st
( y1,y2,z1 is_collinear & p1,p2,z2 is_collinear & q,z1,z2 is_collinear )
consider b, b' being Element of (ProjectiveSpace V) such that
A22: ( y1,y2,b' is_collinear & q1,q2,b is_collinear & q,b',b is_collinear ) by A13;
ex a being Element of (ProjectiveSpace V) st
( p1,p2,a is_collinear & x <> a )

proof

A23: now

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

end;

now

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

end;

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

end;

then consider x1 being Element of (ProjectiveSpace V) such that
A26: ( p1,p2,x1 is_collinear & x <> x1 ) ;
ex a being Element of (ProjectiveSpace V) st
( y1,y2,a is_collinear & b' <> a )

proof

A27: now

assume A28: b' <> y1 ; :: thesis: ex y1, a being Element of (ProjectiveSpace V) st
( y1,y2,a is_collinear & b' <> a )
take y1 = y1; :: thesis: ex a being Element of (ProjectiveSpace V) st
( y1,y2,a is_collinear & b' <> a )
y1,y2,y1 is_collinear by Def7;
hence ex a being Element of (ProjectiveSpace V) st
( y1,y2,a is_collinear & b' <> a ) by A28; :: thesis: verum

end;

now

assume A29: b' <> y2 ; :: thesis: ex y2, a being Element of (ProjectiveSpace V) st
( y1,y2,a is_collinear & b' <> a )
take y2 = y2; :: thesis: ex a being Element of (ProjectiveSpace V) st
( y1,y2,a is_collinear & b' <> a )
y1,y2,y2 is_collinear by Def7;
hence ex a being Element of (ProjectiveSpace V) st
( y1,y2,a is_collinear & b' <> a ) by A29; :: thesis: verum

end;

hence ex a being Element of (ProjectiveSpace V) st
( y1,y2,a is_collinear & b' <> a ) by A21, A27; :: thesis: verum

end;

then consider x3 being Element of (ProjectiveSpace V) such that
A30: ( b' <> x3 & y1,y2,x3 is_collinear ) ;
consider d, d' being Element of (ProjectiveSpace V) such that
A31: ( x1,x3,d' is_collinear & q1,q2,d is_collinear & q,d',d is_collinear ) by A13;
A32: b,d,x is_collinear by A15, A18, A22, A31, Def8;

A33: now

assume A34: b = d ; :: thesis: ex z2, z1 being Element of (ProjectiveSpace V) st
( y1,y2,z1 is_collinear & p1,p2,z2 is_collinear & q,z1,z2 is_collinear )
A35: b,q,b' is_collinear by A22, Th25;
A36: b,q,d' is_collinear by A31, A34, Th25;
b,q,q is_collinear by Def7;
then A37: b',d',q is_collinear by A14, A22, A35, A36, Def8;
d',x3,x1 is_collinear by A31, Th25;
then consider z1 being Element of (ProjectiveSpace V) such that
A38: ( b',x3,z1 is_collinear & q,x1,z1 is_collinear ) by A37, Def9;
( y1,y2,y1 is_collinear & y1,y2,y2 is_collinear ) by Def7;
then ( b',x3,y1 is_collinear & b',x3,y2 is_collinear ) by A21, A22, A30, Def8;
then A39: y1,y2,z1 is_collinear by A30, A38, Def8;
q,z1,x1 is_collinear by A38, Th25;
hence ex z2, z1 being Element of (ProjectiveSpace V) st
( y1,y2,z1 is_collinear & p1,p2,z2 is_collinear & q,z1,z2 is_collinear ) by A26, A39; :: thesis: verum

end;

now

assume A40: b <> d ; :: thesis: ex z2, z1 being Element of (ProjectiveSpace V) st
( y1,y2,z1 is_collinear & p1,p2,z2 is_collinear & q,z1,z2 is_collinear )
not q,b,d is_collinear

proof

assume q,b,d is_collinear ; :: thesis: contradiction
then A41: b,d,q is_collinear by Th25;
A42: b,d,q1 is_collinear

proof

q1,q2,q1 is_collinear by Def7;
hence b,d,q1 is_collinear by A18, A22, A31, Def8; :: thesis: verum

end;

b,d,q2 is_collinear

proof

q1,q2,q2 is_collinear by Def7;
hence b,d,q2 is_collinear by A18, A22, A31, Def8; :: thesis: verum

end;

hence contradiction by A14, A40, A41, A42, Def8; :: thesis: verum

end;

then consider o being Element of (ProjectiveSpace V) such that
A43: ( b',d',o is_collinear & q,x,o is_collinear ) by A22, A31, A32, Lm45;
d',x3,x1 is_collinear by A31, Th25;
then consider z1 being Element of (ProjectiveSpace V) such that
A44: ( b',x3,z1 is_collinear & o,x1,z1 is_collinear ) by A43, Def9;
( x1,o,z1 is_collinear & o,x,q is_collinear ) by A43, A44, Th25;
then consider z2 being Element of (ProjectiveSpace V) such that
A45: ( x1,x,z2 is_collinear & z1,q,z2 is_collinear ) by Def9;
A46: y1,y2,z1 is_collinear

proof

( y1,y2,y1 is_collinear & y1,y2,y2 is_collinear ) by Def7;
then ( b',x3,y1 is_collinear & b',x3,y2 is_collinear ) by A21, A22, A30, Def8;
hence y1,y2,z1 is_collinear by A30, A44, Def8; :: thesis: verum

end;

A47: p1,p2,z2 is_collinear

proof

( p1,p2,p1 is_collinear & p1,p2,p2 is_collinear ) by Def7;
then ( x1,x,p1 is_collinear & x1,x,p2 is_collinear ) by A17, A19, A26, Def8;
hence p1,p2,z2 is_collinear by A26, A45, Def8; :: thesis: verum

end;

q,z1,z2 is_collinear by A45, Th25;
hence ex z2, z1 being Element of (ProjectiveSpace V) st
( y1,y2,z1 is_collinear & p1,p2,z2 is_collinear & q,z1,z2 is_collinear ) by A46, A47; :: thesis: verum

end;

hence ex z2, z1 being Element of (ProjectiveSpace V) st
( y1,y2,z1 is_collinear & p1,p2,z2 is_collinear & q,z1,z2 is_collinear ) by A33; :: thesis: verum

end;

hence ex z2, z1 being Element of (ProjectiveSpace V) st
( y1,y2,z1 is_collinear & p1,p2,z2 is_collinear & q,z1,z2 is_collinear ) by A20; :: thesis: verum

end;

hence S₁[q,p1,p2] ; :: thesis: verum

end;

A48: for q, q1, q2, p1, p2 being Element of (ProjectiveSpace V) st S₁[q,q1,q2] & not q1,q2,q is_collinear & not p1,p2,q is_collinear & ( for x being Element of (ProjectiveSpace V) holds
( not q1,q2,x is_collinear or not p1,p2,x is_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 is_collinear & not p1,p2,q is_collinear & ( for x being Element of (ProjectiveSpace V) holds
( not q1,q2,x is_collinear or not p1,p2,x is_collinear ) ) implies S₁[q,p1,p2] )
assume that
A49: S₁[q,q1,q2] and
A50: not q1,q2,q is_collinear and
A51: not p1,p2,q is_collinear and
A52: for x being Element of (ProjectiveSpace V) holds
( not q1,q2,x is_collinear or not p1,p2,x is_collinear ) ; :: thesis: S₁[q,p1,p2]
consider q3, p3 being Element of (ProjectiveSpace V) such that
A53: ( p1,p2,p3 is_collinear & q1,q2,q3 is_collinear & not q3,p3,q is_collinear ) by A7, A50, A51, A52;
A54: ( q3,p3,q3 is_collinear & q3,p3,p3 is_collinear ) by Def7;
then S₁[q,q3,p3] by A12, A49, A50, A53;
hence S₁[q,p1,p2] by A12, A51, A53, A54; :: thesis: verum

end;

A55: for q, q1, q2 being Element of (ProjectiveSpace V) st S₁[q,q1,q2] & not q1,q2,q is_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 is_collinear implies for p1, p2 being Element of (ProjectiveSpace V) holds S₁[q,p1,p2] )
assume that
A56: S₁[q,q1,q2] and
A57: not q1,q2,q is_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]
A58: ( not p1,p2,q is_collinear & ex x being Element of (ProjectiveSpace V) st
( q1,q2,x is_collinear & p1,p2,x is_collinear ) implies S₁[q,p1,p2] ) by A12, A56, A57;
( not p1,p2,q is_collinear & ( for x being Element of (ProjectiveSpace V) holds
( not q1,q2,x is_collinear or not p1,p2,x is_collinear ) ) implies S₁[q,p1,p2] ) by A48, A56, A57;
hence S₁[q,p1,p2] by A5, A58; :: thesis: verum

end;

A59: for q, q1, q2, x, q3 being Element of (ProjectiveSpace V) st S₁[q,q1,q2] & not q1,q2,q is_collinear & q1,q2,x is_collinear & q,q3,x is_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 is_collinear & q1,q2,x is_collinear & q,q3,x is_collinear implies S₁[q3,q1,q2] )
assume that
A60: S₁[q,q1,q2] and
A61: not q1,q2,q is_collinear and
A62: ( q1,q2,x is_collinear & q,q3,x is_collinear ) ; :: thesis: S₁[q3,q1,q2]

now

let y1, y2 be Element of (ProjectiveSpace V); :: thesis: ex x2, x1 being Element of (ProjectiveSpace V) st
( y1,y2,x1 is_collinear & q1,q2,x2 is_collinear & q3,x1,x2 is_collinear )
consider z2, z1 being Element of (ProjectiveSpace V) such that
A63: ( y1,y2,z1 is_collinear & q1,q2,z2 is_collinear & q,z1,z2 is_collinear ) by A60;

A64: now

assume A65: x = z2 ; :: thesis: ex x2, x1 being Element of (ProjectiveSpace V) st
( y1,y2,x1 is_collinear & q1,q2,x2 is_collinear & q3,x1,x2 is_collinear )
then ( q,x,q3 is_collinear & q,x,z1 is_collinear & q,x,x is_collinear ) by A62, A63, Def7, Th25;
then q3,z1,z2 is_collinear by A61, A62, A65, Def8;
hence ex x2, x1 being Element of (ProjectiveSpace V) st
( y1,y2,x1 is_collinear & q1,q2,x2 is_collinear & q3,x1,x2 is_collinear ) by A63; :: thesis: verum

end;

now

assume A66: x <> z2 ; :: thesis: ex x2, x1 being Element of (ProjectiveSpace V) st
( y1,y2,x1 is_collinear & q1,q2,x2 is_collinear & q3,x1,x2 is_collinear )
( q3,q,x is_collinear & q,z1,z2 is_collinear ) by A62, A63, Th25;
then consider x2 being Element of (ProjectiveSpace V) such that
A67: ( q3,z1,x2 is_collinear & x,z2,x2 is_collinear ) by Def9;
A68: q1 <> q2 by A61, Def7;
( q1,q2,q1 is_collinear & q1,q2,q2 is_collinear ) by Def7;
then ( x,z2,q1 is_collinear & x,z2,q2 is_collinear ) by A62, A63, A68, Def8;
then q1,q2,x2 is_collinear by A66, A67, Def8;
hence ex x2, x1 being Element of (ProjectiveSpace V) st
( y1,y2,x1 is_collinear & q1,q2,x2 is_collinear & q3,x1,x2 is_collinear ) by A63, A67; :: thesis: verum

end;

hence ex x2, x1 being Element of (ProjectiveSpace V) st
( y1,y2,x1 is_collinear & q1,q2,x2 is_collinear & q3,x1,x2 is_collinear ) by A64; :: thesis: verum

end;

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

end;

A69: 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 is_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 is_collinear ) )
assume A70: 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 is_collinear )
consider x1 being Element of (ProjectiveSpace V) such that
A71: ( p <> x1 & q <> x1 & p,q,x1 is_collinear ) by A2;
consider x2 being Element of (ProjectiveSpace V) such that
A72: not p,x1,x2 is_collinear by A1, A71, COLLSP:19;
A73: not x1,x2,p is_collinear by A72, Th25;
A74: not x1,x2,q is_collinear

proof

assume x1,x2,q is_collinear ; :: thesis: contradiction
then ( q,x1,x1 is_collinear & q,x1,x2 is_collinear & q,x1,p is_collinear ) by A71, Def7, Th25;
hence contradiction by A71, A72, Def8; :: thesis: verum

end;

A75: ( x1,x2,x1 is_collinear & q,p,x1 is_collinear ) by A71, Def7, Th25;
S₁[q,x1,x2] by A70;
then S₁[p,x1,x2] by A59, A74, A75;
hence ex p1, p2 being Element of (ProjectiveSpace V) st
( S₁[p,p1,p2] & not p1,p2,p is_collinear ) by A73; :: thesis: verum

end;

A76: 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 is_collinear by A3, Th25;
then for p1, p2 being Element of (ProjectiveSpace V) holds S₁[p,p1,p2] by A4, A55;
then ex r1, r2 being Element of (ProjectiveSpace V) st
( S₁[x,r1,r2] & not r1,r2,x is_collinear ) by A69;
hence S₁[x,y1,z] by A55; :: thesis: verum

end;

A77: for p4, p1, q, q4, r2 being Element of (ProjectiveSpace V) ex r, r1 being Element of (ProjectiveSpace V) st
( p4,q,r is_collinear & p1,q4,r1 is_collinear & r2,r,r1 is_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 is_collinear & p1,q4,r1 is_collinear & r2,r,r1 is_collinear )
ex r1, r being Element of (ProjectiveSpace V) st
( p4,q,r is_collinear & p1,q4,r1 is_collinear & r2,r,r1 is_collinear ) by A76;
hence ex r, r1 being Element of (ProjectiveSpace V) st
( p4,q,r is_collinear & p1,q4,r1 is_collinear & r2,r,r1 is_collinear ) ; :: thesis: verum

end;

reconsider CS = ProjectiveSpace V as CollProjectiveSpace by A1, A2, Def10;
take CS ; :: thesis: ( CS = ProjectiveSpace V & CS is at_most-3-dimensional )
thus ( CS = ProjectiveSpace V & CS is at_most-3-dimensional ) by A77, Def15; :: thesis: verum