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 )
assume A1: 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
consider x, y, z being Element of AS;
consider X being Subset of AS such that
A2: x in X and
( y in X & z in X ) and
A3: X is being_plane by AFF_4:37;
consider t being Element of AS such that
A4: not t in X by A1, A3, AFF_4:48;
set Y = Line x,t;
A5: ( Line x,t is being_line & x in Line x,t & t in Line x,t ) by A2, A4, AFF_1:26, AFF_1:def 3;
then reconsider a = LDir (Line x,t) as Element of the Points of (ProjHorizon AS) by Th14;
reconsider A = PDir X as Element of the Lines of (ProjHorizon AS) by A3, Th15;
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
thus not a on A :: thesis: verum

proof

assume a on A ; :: thesis: contradiction
then Line x,t '||' X by A3, A5, Th36;
then Line x,t c= X by A2, A3, A5, AFF_4:43;
hence contradiction by A4, A5; :: thesis: verum

end;