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 )
consider x, y, z being Element of AS;
consider X being Subset of AS such that
A1: x in X and
y in X and
z 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 x,t;
A4: Line x,t is being_line by A1, A3, AFF_1:def 3;
then reconsider a = LDir (Line x,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 x,t by AFF_1:26;
A6: x in Line x,t by AFF_1:26;
thus not a on A :: thesis: verum

proof

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

end;