theorem :: AFPROJ:45
for AS being AffinSpace st IncProjSp_of AS is 2-dimensional holds
AS is AffinPlane