let AS be AffinSpace; ( 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
; 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
; not for A being Element of the Lines of (ProjHorizon AS) holds a on A
take
A
; 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
verum