consider AS being AffinPlane;
set XX = IncProjSp_of AS;
for A, K being LINE of (IncProjSp_of AS) ex a being POINT of (IncProjSp_of AS) st
( a on A & a on K ) by Lm5;
then IncProjSp_of AS is 2-dimensional IncProjSp by INCPROJ:def 14;
hence ex b₁ being IncProjSp st
( b₁ is strict & b₁ is 2-dimensional ) ; :: thesis: verum