set XX = IncProjSp_of AS;
for A, K being LINE of (IncProjSp_of AS) ex a being Element of the Points of (IncProjSp_of AS) st
( a on A & a on K ) by Lm5;
hence IncProjSp_of AS is 2-dimensional by INCPROJ:def 9; :: thesis: verum