set PS = IncProjSp_of CPS;
A1: for a, b, c, d, p, q being POINT of (IncProjSp_of CPS)
for M, N, P, Q being LINE of (IncProjSp_of CPS) st a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N holds
ex q being POINT of (IncProjSp_of CPS) st
( q on P & q on Q ) by Th13;
A2: ( not for p being POINT of (IncProjSp_of CPS)
for P being LINE of (IncProjSp_of CPS) holds p on P & ( for P being LINE of (IncProjSp_of CPS) ex a, b, c being POINT of (IncProjSp_of CPS) st
( a <> b & b <> c & c <> a & a on P & b on P & c on P ) ) ) by Th11, Th12;
( ( for p, q being POINT of (IncProjSp_of CPS)
for P, Q being LINE of (IncProjSp_of CPS) st p on P & q on P & p on Q & q on Q & not p = q holds
P = Q ) & ( for p, q being POINT of (IncProjSp_of CPS) ex P being LINE of (IncProjSp_of CPS) st
( p on P & q on P ) ) ) by Th8, Th9;
hence ( IncProjSp_of CPS is partial & IncProjSp_of CPS is linear & IncProjSp_of CPS is up-2-dimensional & IncProjSp_of CPS is up-3-rank & IncProjSp_of CPS is Vebleian ) by A2, A1, Def4, Def5, Def6, Def7, Def8; :: thesis: verum