let AS be AffinSpace; not for a being POINT of (IncProjSp_of AS)
for A being LINE of (IncProjSp_of AS) holds a on A
consider x, y, z being Element of AS such that
A1:
not LIN x,y,z
by AFF_1:12;
y <> z
by A1, AFF_1:7;
then A2:
Line (y,z) is being_line
by AFF_1:def 3;
then reconsider A = [(Line (y,z)),1] as LINE of (IncProjSp_of AS) by Th23;
reconsider a = x as POINT of (IncProjSp_of AS) by Th20;
take
a
; not for A being LINE of (IncProjSp_of AS) holds a on A
take
A
; not a on A
thus
not a on A
verum