let AS be AffinSpace; :: thesis: ( ProjHorizon AS is IncProjSp implies not AS is AffinPlane )
set XX = ProjHorizon AS;
assume ProjHorizon AS is IncProjSp ; :: thesis: AS is not AffinPlane
then consider a being Element of the Points of (ProjHorizon AS), A being Element of the Lines of (ProjHorizon AS) such that
A1: not a on A by INCPROJ:def 6;
consider X being Subset of AS such that
A2: a = LDir X and
A3: X is being_line by Th14;
consider Y being Subset of AS such that
A4: A = PDir Y and
A5: Y is being_plane by Th15;
assume AS is AffinPlane ; :: thesis: contradiction
then Y = the carrier of AS by A5, Th2;
then X '||' Y by A3, A5, AFF_4:42;
hence contradiction by A1, A2, A3, A4, A5, Th36; :: thesis: verum