consider V being non trivial RealLinearSpace such that

A2: ex u, v, w, u1 being Element of V st

( ( for a, b, c, d being Real 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 being Real st y = (((a * u) + (b * v)) + (c * w)) + (d * u1) ) ) by Th22;

reconsider V = V as up-3-dimensional RealLinearSpace by A2, Lm42;

take CS = ProjectiveSpace V; :: thesis: ( CS is strict & CS is Fanoian & CS is Desarguesian & CS is Pappian & CS is at_most-3-dimensional & CS is up-3-dimensional )

thus ( CS is strict & CS is Fanoian & CS is Desarguesian & CS is Pappian ) ; :: thesis: ( CS is at_most-3-dimensional & CS is up-3-dimensional )

ex CS being CollProjectiveSpace st

( CS = ProjectiveSpace V & CS is up-3-dimensional & CS is at_most-3-dimensional ) by A2, Th34;

hence ( CS is at_most-3-dimensional & CS is up-3-dimensional ) ; :: thesis: verum

A2: ex u, v, w, u1 being Element of V st

( ( for a, b, c, d being Real 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 being Real st y = (((a * u) + (b * v)) + (c * w)) + (d * u1) ) ) by Th22;

reconsider V = V as up-3-dimensional RealLinearSpace by A2, Lm42;

take CS = ProjectiveSpace V; :: thesis: ( CS is strict & CS is Fanoian & CS is Desarguesian & CS is Pappian & CS is at_most-3-dimensional & CS is up-3-dimensional )

thus ( CS is strict & CS is Fanoian & CS is Desarguesian & CS is Pappian ) ; :: thesis: ( CS is at_most-3-dimensional & CS is up-3-dimensional )

ex CS being CollProjectiveSpace st

( CS = ProjectiveSpace V & CS is up-3-dimensional & CS is at_most-3-dimensional ) by A2, Th34;

hence ( CS is at_most-3-dimensional & CS is up-3-dimensional ) ; :: thesis: verum