theorem :: AFPROJ:45

for AS being AffinSpace st IncProjSp_of AS is 2-dimensional holds
AS is AffinPlane