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