:: Projective Spaces :: by Wojciech Leo\'nczuk and Krzysztof Pra\.zmowski :: :: Received June 15, 1990 :: Copyright (c) 1990-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies RLVECT_1, SUBSET_1, REAL_1, RELAT_1, ARYTM_3, SUPINF_2, CARD_1, XCMPLX_0, ANPROJ_1, ARYTM_1, XBOOLE_0, FUNCT_2, NUMBERS, FUNCT_1, FUNCSDOM, ZFMISC_1, INCSP_1, COLLSP, RELAT_2, VECTSP_1, AFF_2, ANALOAF, ANPROJ_2, FUNCT_7, PENCIL_1; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, FUNCT_1, FUNCT_2, BINOP_1, DOMAIN_1, XCMPLX_0, XREAL_0, STRUCT_0, RLVECT_1, REAL_1, FUNCSDOM, COLLSP, ANPROJ_1; constructors DOMAIN_1, REAL_1, FUNCSDOM, BINOP_2, ANPROJ_1, RELSET_1, VALUED_2, NUMBERS; registrations XBOOLE_0, SUBSET_1, RELSET_1, NUMBERS, STRUCT_0, COLLSP, ANPROJ_1, XREAL_0, ORDINAL1; requirements NUMERALS, SUBSET, BOOLE, ARITHM; begin reserve V for RealLinearSpace, o,p,q,r,s,u,v,w,y,y1,u1,v1,w1,u2,v2,w2 for Element of V, a,b,c,d,a1,b1,c1,d1,a2,b2,c2,d2,a3,b3,c3,d3 for Real, z for set; theorem :: ANPROJ_2:1 (for a,b,c st a*u + b*v + c*w = 0.V holds a = 0 & b = 0 & c = 0) implies u is not zero & v is not zero & w is not zero & not u,v,w are_LinDep & not are_Prop u,v; theorem :: ANPROJ_2:2 for u,v,u1,v1 holds ((for a,b,a1,b1 st a*u + b*v + a1*u1 + b1*v1 = 0.V holds a=0 & b=0 & a1=0 & b1=0) implies u is not zero & v is not zero & not are_Prop u,v & u1 is not zero & v1 is not zero & not are_Prop u1,v1 & not u ,v,u1 are_LinDep & not u1,v1,u are_LinDep); theorem :: ANPROJ_2:3 (for w ex a,b,c st w = a*p + b*q + c*r) & (for a,b,c st a*p + b*q + c*r = 0.V holds a = 0 & b = 0 & c = 0) implies for u,u1 ex y st p,q,y are_LinDep & u,u1,y are_LinDep & y is not zero; theorem :: ANPROJ_2:4 (for w ex a,b,c,d st w = a*p + b*q + c*r + d*s) & (for a,b,c,d st a*p + b*q + c*r + d*s = 0.V holds a = 0 & b = 0 & c = 0 & d = 0) implies for u, v st u is not zero & v is not zero ex y,w st u,v,w are_LinDep & q,r,y are_LinDep & p,w,y are_LinDep & y is not zero & w is not zero; theorem :: ANPROJ_2:5 (for a,b,a1,b1 st a*u + b*v + a1*u1 + b1*v1 = 0.V holds a=0 & b=0 & a1=0 & b1=0) implies not ex y st y is not zero & u,v,y are_LinDep & u1,v1,y are_LinDep; definition let V,u,v,w; pred u,v,w are_Prop_Vect means :: ANPROJ_2:def 1 u is not zero & v is not zero & w is not zero; end; definition let V,u,v,w,u1,v1,w1; pred u,v,w,u1,v1,w1 lie_on_a_triangle means :: ANPROJ_2:def 2 u,v,w1 are_LinDep & u,w, v1 are_LinDep & v,w,u1 are_LinDep; end; definition let V,o,u,v,w,u2,v2,w2; pred o,u,v,w,u2,v2,w2 are_perspective means :: ANPROJ_2:def 3 o,u,u2 are_LinDep & o,v, v2 are_LinDep & o,w,w2 are_LinDep; end; theorem :: ANPROJ_2:6 o,u,u2 are_LinDep & not are_Prop o,u & not are_Prop o,u2 & not are_Prop u,u2 & o,u,u2 are_Prop_Vect implies (ex a1,b1 st b1*u2=o+a1*u & a1<>0 & b1<>0) & ex a2,c2 st u2=c2*o+a2*u & c2<>0 & a2<>0; theorem :: ANPROJ_2:7 p,q,r are_LinDep & not are_Prop p,q & p,q,r are_Prop_Vect implies ex a,b st r = a*p + b*q; theorem :: ANPROJ_2:8 o is not zero & u,v,w are_Prop_Vect & u2,v2,w2 are_Prop_Vect & u1 ,v1,w1 are_Prop_Vect & o,u,v,w,u2,v2,w2 are_perspective & not are_Prop o,u2 & not are_Prop o,v2 & not are_Prop o,w2 & not are_Prop u,u2 & not are_Prop v,v2 & not are_Prop w,w2 & not o,u,v are_LinDep & not o,u,w are_LinDep & not o,v,w are_LinDep & u,v,w,u1,v1,w1 lie_on_a_triangle & u2,v2,w2,u1,v1,w1 lie_on_a_triangle implies u1,v1,w1 are_LinDep; definition let V,o,u,v,w,u2,v2,w2; pred o,u,v,w,u2,v2,w2 lie_on_an_angle means :: ANPROJ_2:def 4 not o,u,u2 are_LinDep & o ,u,v are_LinDep & o,u,w are_LinDep & o,u2,v2 are_LinDep & o,u2,w2 are_LinDep; end; definition let V,o,u,v,w,u2,v2,w2; pred o,u,v,w,u2,v2,w2 are_half_mutually_not_Prop means :: ANPROJ_2:def 5 not are_Prop o ,v & not are_Prop o,w & not are_Prop o,v2 & not are_Prop o,w2 & not are_Prop u, v & not are_Prop u,w & not are_Prop u2,v2 & not are_Prop u2,w2 & not are_Prop v ,w & not are_Prop v2,w2; end; theorem :: ANPROJ_2:9 o is not zero & u,v,w are_Prop_Vect & u2,v2,w2 are_Prop_Vect & u1 ,v1,w1 are_Prop_Vect & o,u,v,w,u2,v2,w2 lie_on_an_angle & o,u,v,w,u2,v2,w2 are_half_mutually_not_Prop & u,v2,w1 are_LinDep & u2,v,w1 are_LinDep & u,w2,v1 are_LinDep & w,u2,v1 are_LinDep & v,w2,u1 are_LinDep & w,v2,u1 are_LinDep implies u1,v1,w1 are_LinDep; reserve A for non empty set; reserve f,g,h,f1 for Element of Funcs(A,REAL); reserve x1,x2,x3,x4 for Element of A; theorem :: ANPROJ_2:10 ex f st f.x1 = 1 & for z st z in A & z<>x1 holds f.z = 0; theorem :: ANPROJ_2:11 x1<>x2 & x1<>x3 & x2<>x3 & f.x1 = 1 & (for z st z in A holds(z<> x1 implies f.z = 0)) & g.x2 = 1 & (for z st z in A holds(z<>x2 implies g.z = 0) ) & h.x3 = 1 & (for z st z in A holds(z<>x3 implies h.z = 0)) implies for a,b,c being Real st (RealFuncAdd(A)).((RealFuncAdd(A)). ((RealFuncExtMult(A)).[a,f],( RealFuncExtMult(A)).[b,g]), (RealFuncExtMult(A)).[c,h]) = RealFuncZero(A) holds a=0 & b=0 & c = 0; theorem :: ANPROJ_2:12 x1<>x2 & x1<>x3 & x2<>x3 implies ex f,g,h st for a,b,c being Real st (RealFuncAdd (A)).((RealFuncAdd(A)). ((RealFuncExtMult(A)).[a,f],(RealFuncExtMult(A)).[b,g]) , (RealFuncExtMult(A)).[c,h]) = RealFuncZero(A) holds a=0 & b=0 & c = 0; theorem :: ANPROJ_2:13 A = {x1,x2,x3} & x1<>x2 & x1<>x3 & x2<>x3 & f.x1 = 1 & (for z st z in A holds (z<>x1 implies f.z = 0)) & g.x2 = 1 & (for z st z in A holds (z<> x2 implies g.z = 0)) & h.x3 = 1 & (for z st z in A holds (z<>x3 implies h.z = 0 )) implies for h9 being Element of Funcs(A,REAL) holds ex a,b,c being Real st h9 = ( RealFuncAdd(A)).((RealFuncAdd(A)). ((RealFuncExtMult(A)).[a,f],(RealFuncExtMult (A)).[b,g]), (RealFuncExtMult(A)).[c,h]); theorem :: ANPROJ_2:14 A = {x1,x2,x3} & x1<>x2 & x1<>x3 & x2<>x3 implies ex f,g,h st for h9 being Element of Funcs(A,REAL) ex a,b,c being Real st h9 = (RealFuncAdd(A)).(( RealFuncAdd(A)). ((RealFuncExtMult(A)).[a,f],(RealFuncExtMult(A)).[b,g]), ( RealFuncExtMult(A)).[c,h]); theorem :: ANPROJ_2:15 A = {x1,x2,x3} & x1<>x2 & x1<>x3 & x2<>x3 implies ex f,g,h st ( for a,b,c being Real st (RealFuncAdd(A)).((RealFuncAdd(A)). ((RealFuncExtMult(A)).[a,f],( RealFuncExtMult(A)).[b,g]), (RealFuncExtMult(A)).[c,h]) = RealFuncZero(A) holds a=0 & b=0 & c = 0) & for h9 being Element of Funcs(A,REAL) ex a,b,c being Real st h9 = (RealFuncAdd(A)).((RealFuncAdd(A)). ((RealFuncExtMult(A)).[a,f],( RealFuncExtMult(A)).[b,g]), (RealFuncExtMult(A)).[c,h]); theorem :: ANPROJ_2:16 ex V being non trivial RealLinearSpace st ex u,v,w being Element of V st (for a,b,c st a*u + b*v + c*w = 0.V holds a=0 & b=0 & c = 0) & for y being Element of V ex a,b,c st y = a*u + b*v + c*w; theorem :: ANPROJ_2:17 x1<>x2 & x1<>x3 & x1<>x4 & x2<>x3 & x2<>x4 & x3<>x4 & f.x1 = 1 & (for z st z in A holds(z<>x1 implies f.z = 0)) & g.x2 = 1 & (for z st z in A holds(z<>x2 implies g.z = 0)) & h.x3 = 1 & (for z st z in A holds(z<>x3 implies h.z = 0)) & f1.x4 = 1 & (for z st z in A holds(z<>x4 implies f1.z = 0)) implies for a,b,c,d being Real st (RealFuncAdd(A)).((RealFuncAdd(A)).((RealFuncAdd(A)). (( RealFuncExtMult(A)).[a,f],(RealFuncExtMult(A)).[b,g]), (RealFuncExtMult(A)).[c, h]),(RealFuncExtMult(A)).[d,f1]) = RealFuncZero(A) holds a=0 & b=0 & c = 0 & d= 0; theorem :: ANPROJ_2:18 x1<>x2 & x1<>x3 & x1<>x4 & x2<>x3 & x2<>x4 & x3<>x4 implies ex f,g,h, f1 st for a,b,c,d being Real st (RealFuncAdd(A)).((RealFuncAdd(A)).((RealFuncAdd(A)). (( RealFuncExtMult(A)).[a,f],(RealFuncExtMult(A)).[b,g]), (RealFuncExtMult(A)).[c, h]),(RealFuncExtMult(A)).[d,f1]) = RealFuncZero(A) holds a = 0 & b = 0 & c = 0 & d = 0; theorem :: ANPROJ_2:19 A = {x1,x2,x3,x4} & x1<>x2 & x1<>x3 & x1<>x4 & x2<>x3 & x2<>x4 & x3<>x4 & f.x1 = 1 & (for z st z in A holds(z<>x1 implies f.z = 0)) & g.x2 = 1 & (for z st z in A holds(z<>x2 implies g.z = 0)) & h.x3 = 1 & (for z st z in A holds(z<>x3 implies h.z = 0)) & f1.x4 = 1 & (for z st z in A holds(z<>x4 implies f1.z = 0)) implies for h9 being Element of Funcs(A,REAL) ex a,b,c ,d being Real st h9 = (RealFuncAdd(A)).((RealFuncAdd(A)).((RealFuncAdd(A)). (( RealFuncExtMult(A)).[a,f],(RealFuncExtMult(A)).[b,g]), (RealFuncExtMult(A)).[c, h]),(RealFuncExtMult(A)).[d,f1]); theorem :: ANPROJ_2:20 A = {x1,x2,x3,x4} & x1<>x2 & x1<>x3 & x1<>x4 & x2<>x3 & x2<>x4 & x3<> x4 implies ex f,g,h,f1 st for h9 being Element of Funcs(A,REAL) ex a,b,c,d being Real st h9 = (RealFuncAdd(A)).((RealFuncAdd(A)).((RealFuncAdd(A)). (( RealFuncExtMult(A)).[a,f],(RealFuncExtMult(A)).[b,g]), (RealFuncExtMult(A)).[c, h]),(RealFuncExtMult(A)).[d,f1]); theorem :: ANPROJ_2:21 A = {x1,x2,x3,x4} & x1<>x2 & x1<>x3 & x1<>x4 & x2<>x3 & x2<>x4 & x3<>x4 implies ex f,g,h,f1 st (for a,b,c,d being Real st (RealFuncAdd(A)).((RealFuncAdd(A) ).((RealFuncAdd(A)). ((RealFuncExtMult(A)).[a,f],(RealFuncExtMult(A)).[b,g]), ( RealFuncExtMult(A)).[c,h]),(RealFuncExtMult(A)).[d,f1]) = RealFuncZero(A) holds a = 0 & b = 0 & c = 0 & d = 0) & for h9 being Element of Funcs(A,REAL) ex a,b,c,d being Real st h9 = (RealFuncAdd(A)).((RealFuncAdd(A)).((RealFuncAdd(A)). (( RealFuncExtMult(A)).[a,f],(RealFuncExtMult(A)).[b,g]), (RealFuncExtMult(A)).[c, h]),(RealFuncExtMult(A)).[d,f1]); theorem :: ANPROJ_2:22 ex V being non trivial RealLinearSpace st ex u,v,w,u1 being Element of V st (for a,b,c,d st a*u + b*v + c*w + d*u1 = 0.V holds a = 0 & b = 0 & c = 0 & d = 0) & for y being Element of V ex a,b,c,d st y = a*u + b*v + c*w + d*u1; definition let IT be RealLinearSpace; attr IT is up-3-dimensional means :: ANPROJ_2:def 6 ex u,v,w1 being Element of IT st for a,b,c st a*u + b*v + c*w1 = 0.IT holds a = 0 & b = 0 & c = 0; end; registration cluster up-3-dimensional for RealLinearSpace; end; registration cluster up-3-dimensional -> non trivial for RealLinearSpace; end; definition let CS be non empty CollStr; redefine attr CS is reflexive means :: ANPROJ_2:def 7 for p,q,r being Element of CS holds p,q,p are_collinear & p,p,q are_collinear & p,q,q are_collinear; redefine attr CS is transitive means :: ANPROJ_2:def 8 for p,q,r,r1,r2 being Element of CS st p <>q & p,q,r are_collinear & p,q,r1 are_collinear & p,q,r2 are_collinear holds r,r1,r2 are_collinear; end; definition let IT be non empty CollStr; attr IT is Vebleian means :: ANPROJ_2:def 9 for p,p1,p2,r,r1 being Element of IT st p, p1,r are_collinear & p1,p2,r1 are_collinear ex r2 being Element of IT st p,p2,r2 are_collinear & r,r1,r2 are_collinear; attr IT is at_least_3rank means :: ANPROJ_2:def 10 for p,q being Element of IT ex r being Element of IT st p<>r & q<>r & p,q,r are_collinear; end; reserve V for non trivial RealLinearSpace; reserve u,v,w,y,u1,v1,w1,u2,w2 for Element of V; reserve p,p1,p2,p3,q,q1,q2,q3,r,r1,r2,r3 for Element of ProjectiveSpace(V); theorem :: ANPROJ_2:23 p,q,r are_collinear iff ex u,v,w st p = Dir(u) & q = Dir(v) & r = Dir(w) & u is not zero & v is not zero & w is not zero & u,v,w are_LinDep; registration let V; cluster ProjectiveSpace V -> reflexive transitive; end; theorem :: ANPROJ_2:24 p,q,r are_collinear implies p,r,q are_collinear & q,p,r are_collinear & r,q,p are_collinear & r,p,q are_collinear & q,r,p are_collinear; registration let V; cluster ProjectiveSpace(V) -> Vebleian; end; registration let V be up-3-dimensional RealLinearSpace; cluster ProjectiveSpace(V) -> proper; end; theorem :: ANPROJ_2:25 (ex u,v st for a,b st a*u + b*v = 0.V holds a = 0 & b = 0 ) implies ProjectiveSpace(V) is at_least_3rank; registration let V be up-3-dimensional RealLinearSpace; cluster ProjectiveSpace(V) -> at_least_3rank; end; registration cluster transitive reflexive proper Vebleian at_least_3rank for non empty CollStr; end; definition mode CollProjectiveSpace is reflexive transitive Vebleian at_least_3rank proper non empty CollStr; end; definition let IT be non empty CollStr; attr IT is Fanoian means :: ANPROJ_2:def 11 for p1,r2,q,r1,q1,p,r being Element of IT holds (p1,r2,q are_collinear & r1,q1,q are_collinear & p1,r1,p are_collinear & r2, q1,p are_collinear & p1,q1,r are_collinear & r2,r1,r are_collinear & p,q,r are_collinear implies (p1,r2,q1 are_collinear or p1,r2,r1 are_collinear or p1,r1, q1 are_collinear or r2,r1,q1 are_collinear)); attr IT is Desarguesian means :: ANPROJ_2:def 12 for o,p1,p2,p3,q1,q2,q3,r1,r2,r3 being Element of IT st o<>q1 & p1<>q1 & o<>q2 & p2<>q2 & o<>q3 & p3<>q3 & not o,p1,p2 are_collinear & not o,p1,p3 are_collinear & not o,p2,p3 are_collinear & p1,p2,r3 are_collinear & q1,q2,r3 are_collinear & p2,p3,r1 are_collinear & q2,q3,r1 are_collinear & p1,p3,r2 are_collinear & q1,q3,r2 are_collinear & o,p1,q1 are_collinear & o,p2,q2 are_collinear & o,p3,q3 are_collinear holds r1,r2,r3 are_collinear; attr IT is Pappian means :: ANPROJ_2:def 13 for o,p1,p2,p3,q1,q2,q3,r1,r2,r3 being Element of IT st o<>p2 & o<>p3 & p2<>p3 & p1<>p2 & p1<>p3 & o<>q2 & o<>q3 & q2<>q3 & q1<> q2 & q1<>q3 & not o,p1,q1 are_collinear & o,p1,p2 are_collinear & o,p1,p3 are_collinear & o,q1,q2 are_collinear & o,q1,q3 are_collinear & p1,q2,r3 are_collinear & q1,p2,r3 are_collinear & p1,q3,r2 are_collinear & p3,q1,r2 are_collinear & p2,q3,r1 are_collinear & p3,q2,r1 are_collinear holds r1,r2,r3 are_collinear; end; definition let IT be CollProjectiveSpace; attr IT is 2-dimensional means :: ANPROJ_2:def 14 for p,p1,q,q1 being Element of IT ex r being Element of IT st p,p1,r are_collinear & q,q1,r are_collinear; end; notation let IT be CollProjectiveSpace; antonym IT is up-3-dimensional for IT is 2-dimensional; end; definition let IT be CollProjectiveSpace; attr IT is at_most-3-dimensional means :: ANPROJ_2:def 15 for p,p1,q,q1,r2 being Element of IT ex r,r1 being Element of IT st p,q,r are_collinear & p1,q1,r1 are_collinear & r2,r,r1 are_collinear; end; theorem :: ANPROJ_2:26 p1,r2,q are_collinear & r1,q1,q are_collinear & p1,r1,p are_collinear & r2,q1,p are_collinear & p1,q1,r are_collinear & r2,r1,r are_collinear & p,q,r are_collinear implies (p1,r2,q1 are_collinear or p1,r2,r1 are_collinear or p1,r1,q1 are_collinear or r2,r1,q1 are_collinear); registration let V be up-3-dimensional RealLinearSpace; ::$N Desargues' Theorem cluster ProjectiveSpace V -> Fanoian Desarguesian Pappian; end; theorem :: ANPROJ_2:27 (ex u,v,w st (for a,b,c st a*u + b*v + c*w = 0.V holds a=0 & b=0 & c = 0) & (for y ex a,b,c st y = a*u + b*v + c*w)) implies ex x1,x2 being Element of ProjectiveSpace(V) st (x1<>x2 & for r1,r2 ex q st x1,x2,q are_collinear & r1,r2,q are_collinear); theorem :: ANPROJ_2:28 (ex x1,x2 being Element of ProjectiveSpace(V) st (x1<>x2 & for r1,r2 ex q st x1,x2,q are_collinear & r1,r2,q are_collinear)) implies for p,p1,q, q1 ex r st p,p1,r are_collinear & q,q1,r are_collinear; theorem :: ANPROJ_2:29 (ex u,v,w st (for a,b,c st a*u + b*v + c*w = 0.V holds a=0 & b=0 & c = 0) & (for y ex a,b,c st y = a*u + b*v + c*w)) implies ex CS being CollProjectiveSpace st CS = ProjectiveSpace(V) & CS is 2-dimensional; theorem :: ANPROJ_2:30 (ex y,u,v,w st (for w1 ex a,b,a1,b1 st w1 = a*y + b*u + a1*v + b1*w) & (for a,b,a1,b1 st a*y + b*u + a1*v + b1*w = 0.V holds a=0 & b=0 & a1=0 & b1=0)) implies ex p,q1,q2 st not p,q1,q2 are_collinear & for r1,r2 ex q3,r3 st r1,r2,r3 are_collinear & q1,q2,q3 are_collinear & p,r3,q3 are_collinear; reserve x,z,x1,y1,z1,x2,x3,y2,z2,p4,q4 for Element of ProjectiveSpace(V); theorem :: ANPROJ_2:31 ProjectiveSpace(V) is proper at_least_3rank & (ex p,q1,q2 st not p,q1,q2 are_collinear & (for r1,r2 ex q3,r3 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; theorem :: ANPROJ_2:32 (ex y,u,v,w st (for w1 ex a,b,c,c1 st w1 = a*y + b*u + c*v + c1* w) & (for a,b,a1,b1 st a*y + b*u + a1*v + b1*w = 0.V holds a=0 & b=0 & a1=0 & b1=0)) implies ex CS being CollProjectiveSpace st CS = ProjectiveSpace(V) & CS is at_most-3-dimensional; theorem :: ANPROJ_2:33 (ex u,v,u1,v1 st (for a,b,a1,b1 st a*u + b*v + a1*u1 + b1*v1 = 0.V holds a=0 & b=0 & a1=0 & b1=0)) implies ex CS being CollProjectiveSpace st CS = ProjectiveSpace(V) & CS is non 2-dimensional; theorem :: ANPROJ_2:34 (ex u,v,u1,v1 st (for w ex a,b,a1,b1 st w = a*u + b*v + a1*u1 + b1*v1) & (for a,b,a1,b1 st a*u + b*v + a1*u1 + b1*v1 = 0.V holds a=0 & b=0 & a1 =0 & b1=0)) implies ex CS being CollProjectiveSpace st CS = ProjectiveSpace(V) & CS is up-3-dimensional at_most-3-dimensional; registration cluster strict Fanoian Desarguesian Pappian 2-dimensional for CollProjectiveSpace; cluster strict Fanoian Desarguesian Pappian at_most-3-dimensional up-3-dimensional for CollProjectiveSpace; end; definition mode CollProjectivePlane is 2-dimensional CollProjectiveSpace; end; theorem :: ANPROJ_2:35 for CS being non empty CollStr holds CS is 2-dimensional CollProjectiveSpace iff (CS is at_least_3rank proper CollSp & for p,p1,q,q1 being Element of CS ex r being Element of CS st p,p1,r are_collinear & q,q1,r are_collinear);