consider V being non trivial RealLinearSpace such that

A1: ex u, v, w being Element of V st

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

reconsider V = V as up-3-dimensional RealLinearSpace by A1, Def6;

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

thus ( CS is strict & CS is Fanoian & CS is Desarguesian & CS is Pappian ) ; :: thesis: CS is 2-dimensional

ex CS1 being CollProjectiveSpace st

( CS1 = ProjectiveSpace V & CS1 is 2-dimensional ) by A1, Th29;

hence CS is 2-dimensional ; :: thesis: verum

A1: ex u, v, w being Element of V st

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

reconsider V = V as up-3-dimensional RealLinearSpace by A1, Def6;

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

thus ( CS is strict & CS is Fanoian & CS is Desarguesian & CS is Pappian ) ; :: thesis: CS is 2-dimensional

ex CS1 being CollProjectiveSpace st

( CS1 = ProjectiveSpace V & CS1 is 2-dimensional ) by A1, Th29;

hence CS is 2-dimensional ; :: thesis: verum