let AS be AffinSpace; :: thesis: ( AS is not AffinPlane implies ex a being Element of the Points of (ProjHorizon AS) ex A being Element of the Lines of (ProjHorizon AS) st not a on A )
set x = the Element of AS;
consider X being Subset of AS such that
A1: the Element of AS in X and
the Element of AS in X and
the Element of AS in X and
A2: X is being_plane by AFF_4:37;
reconsider A = PDir X as Element of the Lines of (ProjHorizon AS) by A2, Th15;
assume AS is not AffinPlane ; :: thesis: not for a being Element of the Points of (ProjHorizon AS)
for A being Element of the Lines of (ProjHorizon AS) holds a on A
then consider t being Element of AS such that
A3: not t in X by A2, AFF_4:48;
set Y = Line ( the Element of AS,t);
A4: Line ( the Element of AS,t) is being_line by A1, A3, AFF_1:def 3;
then reconsider a = LDir (Line ( the Element of AS,t)) as Element of the Points of (ProjHorizon AS) by Th14;
take a ; :: thesis: not for A being Element of the Lines of (ProjHorizon AS) holds a on A
take A ; :: thesis: not a on A
A5: t in Line ( the Element of AS,t) by AFF_1:15;
A6: the Element of AS in Line ( the Element of AS,t) by AFF_1:15;
thus not a on A :: thesis: verum

proof

assume a on A ; :: thesis: contradiction
then Line ( the Element of AS,t) '||' X by A2, A4, Th36;
then Line ( the Element of AS,t) c= X by A1, A2, A4, A6, AFF_4:43;
hence contradiction by A3, A5; :: thesis: verum

end;