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