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_{1}[ 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_{1}[p,q1,q2]
_{1}[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_{1}[q,p1,p2]

( 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 )_{1}[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_{1}[q,p1,p2]
_{1}[q,q1,q2] & not q1,q2,q are_collinear holds

for p1, p2 being Element of (ProjectiveSpace V) holds S_{1}[q,p1,p2]

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_{1}[q,q1,q2] & not q1,q2,q are_collinear & q1,q2,x are_collinear & q,q3,x are_collinear holds

S_{1}[q3,q1,q2]
_{1}[q,q1,q2] ) holds

ex p1, p2 being Element of (ProjectiveSpace V) st

( S_{1}[p,p1,p2] & not p1,p2,p are_collinear )
_{1}[x,y1,z]

( p4,q,r are_collinear & p1,q4,r1 are_collinear & r2,r,r1 are_collinear )

( 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

( 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

proof

A5:
for q, q1, q2, p1, p2, x being Element of (ProjectiveSpace V) st S
let p, q1, q2 be Element of (ProjectiveSpace V); :: thesis: ( q1,q2,p are_collinear implies S_{1}[p,q1,q2] )

assume A4: q1,q2,p are_collinear ; :: thesis: S_{1}[p,q1,q2]

_{1}[p,q1,q2]
; :: thesis: verum

end;assume A4: q1,q2,p are_collinear ; :: thesis: S

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 )

hence
S( 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;( 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

S

proof

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
let q, q1, q2, p1, p2, x be Element of (ProjectiveSpace V); :: thesis: ( S_{1}[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_{1}[q,p1,p2] )

assume that

A6: S_{1}[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_{1}[q,p1,p2]

A11: q1 <> q2 by A7, Def7;

A12: p1 <> p2 by A9, Def7;

_{1}[q,p1,p2]
; :: thesis: verum

end;assume that

A6: S

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

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 )

hence
S( 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 )

( y1,y2,z1 are_collinear & p1,p2,z2 are_collinear & q,z1,z2 are_collinear ) by A13; :: thesis: verum

end;( 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 ) )

( 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 )

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 )

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;

( y1,y2,z1 are_collinear & p1,p2,z2 are_collinear & q,z1,z2 are_collinear ) by A32; :: thesis: verum

end;( p1,p2,a are_collinear & x <> a )

proof

( p1,p2,a are_collinear & x <> a ) by A9, A14, Def7; :: thesis: verum

end;

then consider x1 being Element of (ProjectiveSpace V) such that A14: now :: thesis: ( x <> p2 implies ex p2, a being Element of (ProjectiveSpace V) st

( p1,p2,a are_collinear & x <> a ) )

( 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;( 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

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

( p1,p2,a are_collinear & x <> a ) )

hence
ex 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;( 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

( p1,p2,a are_collinear & x <> a ) by A9, A14, Def7; :: thesis: verum

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

( y1,y2,a are_collinear & b9 <> a ) by A22, A23; :: thesis: verum

end;

then consider x3 being Element of (ProjectiveSpace V) such that A23: now :: thesis: ( b9 <> y2 implies ex y2, a being Element of (ProjectiveSpace V) st

( y1,y2,a are_collinear & b9 <> a ) )

( 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;( 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

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

( y1,y2,a are_collinear & b9 <> a ) )

hence
ex 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;( 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

( y1,y2,a are_collinear & b9 <> a ) by A22, A23; :: thesis: verum

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 ) )

( 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

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;( y1,y2,z1 are_collinear & p1,p2,z2 are_collinear & q,z1,z2 are_collinear )

not q,b,d are_collinear

proof

then consider o being Element of (ProjectiveSpace V) such that
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 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

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

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 ) )

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 ) )

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;( 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

( y1,y2,z1 are_collinear & p1,p2,z2 are_collinear & q,z1,z2 are_collinear ) by A32; :: thesis: verum

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 ) )

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 ) )

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;( 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

( y1,y2,z1 are_collinear & p1,p2,z2 are_collinear & q,z1,z2 are_collinear ) by A13; :: thesis: verum

( 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

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

( 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;( 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

A60:
p1,p2,p2 are_collinear
by Def7;
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;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

( 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

( not q1,q2,x are_collinear or not p1,p2,x are_collinear ) ) holds

S

proof

A70:
for q, q1, q2 being Element of (ProjectiveSpace V) st S
let q, q1, q2, p1, p2 be Element of (ProjectiveSpace V); :: thesis: ( S_{1}[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_{1}[q,p1,p2] )

assume that

A62: S_{1}[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_{1}[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_{1}[q,q3,p3]
by A5, A62, A63, A67, A68;

q3,p3,p3 are_collinear by Def7;

hence S_{1}[q,p1,p2]
by A5, A64, A66, A68, A69; :: thesis: verum

end;( not q1,q2,x are_collinear or not p1,p2,x are_collinear ) ) implies S

assume that

A62: S

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

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

q3,p3,p3 are_collinear by Def7;

hence S

for p1, p2 being Element of (ProjectiveSpace V) holds S

proof

reconsider CS = ProjectiveSpace V as CollProjectiveSpace by A1, A2, Def10;
let q, q1, q2 be Element of (ProjectiveSpace V); :: thesis: ( S_{1}[q,q1,q2] & not q1,q2,q are_collinear implies for p1, p2 being Element of (ProjectiveSpace V) holds S_{1}[q,p1,p2] )

assume A71: ( S_{1}[q,q1,q2] & not q1,q2,q are_collinear )
; :: thesis: for p1, p2 being Element of (ProjectiveSpace V) holds S_{1}[q,p1,p2]

let p1, p2 be Element of (ProjectiveSpace V); :: thesis: S_{1}[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_{1}[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_{1}[q,p1,p2] )
by A5, A71;

hence S_{1}[q,p1,p2]
by A3, A72; :: thesis: verum

end;assume A71: ( S

let p1, p2 be Element of (ProjectiveSpace V); :: thesis: S

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

( 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

hence S

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

S

proof

A91:
for q, p being Element of (ProjectiveSpace V) st ( for q1, q2 being Element of (ProjectiveSpace V) holds S
let q, q1, q2, x, q3 be Element of (ProjectiveSpace V); :: thesis: ( S_{1}[q,q1,q2] & not q1,q2,q are_collinear & q1,q2,x are_collinear & q,q3,x are_collinear implies S_{1}[q3,q1,q2] )

assume that

A76: S_{1}[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_{1}[q3,q1,q2]

_{1}[q3,q1,q2]
; :: thesis: verum

end;assume that

A76: S

A77: not q1,q2,q are_collinear and

A78: q1,q2,x are_collinear and

A79: q,q3,x are_collinear ; :: thesis: S

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 )

hence
S( 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;

( y1,y2,x1 are_collinear & q1,q2,x2 are_collinear & q3,x1,x2 are_collinear ) by A83; :: thesis: verum

end;( 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 ) )

( 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;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

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 ) )

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 ) )

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;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

( y1,y2,x1 are_collinear & q1,q2,x2 are_collinear & q3,x1,x2 are_collinear ) by A83; :: thesis: verum

ex p1, p2 being Element of (ProjectiveSpace V) st

( S

proof

A102:
for x, y1, z being Element of (ProjectiveSpace V) holds S
let q, p be Element of (ProjectiveSpace V); :: thesis: ( ( for q1, q2 being Element of (ProjectiveSpace V) holds S_{1}[q,q1,q2] ) implies ex p1, p2 being Element of (ProjectiveSpace V) st

( S_{1}[p,p1,p2] & not p1,p2,p are_collinear ) )

assume A92: for q1, q2 being Element of (ProjectiveSpace V) holds S_{1}[q,q1,q2]
; :: thesis: ex p1, p2 being Element of (ProjectiveSpace V) st

( S_{1}[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

A100: not x1,x2,p are_collinear by A96, Th24;

A101: S_{1}[q,x1,x2]
by A92;

q,p,x1 are_collinear by A95, Th24;

then S_{1}[p,x1,x2]
by A75, A97, A99, A101;

hence ex p1, p2 being Element of (ProjectiveSpace V) st

( S_{1}[p,p1,p2] & not p1,p2,p are_collinear )
by A100; :: thesis: verum

end;( S

assume A92: for q1, q2 being Element of (ProjectiveSpace V) holds S

( S

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

A99:
x1,x2,x1 are_collinear
by Def7;
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;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

A100: not x1,x2,p are_collinear by A96, Th24;

A101: S

q,p,x1 are_collinear by A95, Th24;

then S

hence ex p1, p2 being Element of (ProjectiveSpace V) st

( S

proof

for p4, p1, q, q4, r2 being Element of (ProjectiveSpace V) ex r, r1 being Element of (ProjectiveSpace V) st
let x, y1, z be Element of (ProjectiveSpace V); :: thesis: S_{1}[x,y1,z]

not q1,q2,p are_collinear by A73, Th24;

then for p1, p2 being Element of (ProjectiveSpace V) holds S_{1}[p,p1,p2]
by A74, A70;

then ex r1, r2 being Element of (ProjectiveSpace V) st

( S_{1}[x,r1,r2] & not r1,r2,x are_collinear )
by A91;

hence S_{1}[x,y1,z]
by A70; :: thesis: verum

end;not q1,q2,p are_collinear by A73, Th24;

then for p1, p2 being Element of (ProjectiveSpace V) holds S

then ex r1, r2 being Element of (ProjectiveSpace V) st

( S

hence S

( p4,q,r are_collinear & p1,q4,r1 are_collinear & r2,r,r1 are_collinear )

proof

hence
( CS = ProjectiveSpace V & CS is at_most-3-dimensional )
; :: thesis: verum
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;( 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