let AS be AffinSpace; :: thesis: 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:21;
y <> z by A1, AFF_1:16;
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 ; :: thesis: not for A being LINE of (IncProjSp_of 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 A3: x in Line y,z by Th26;
A4: z in Line y,z by AFF_1:26;
y in Line y,z by AFF_1:26;
hence contradiction by A1, A2, A3, A4, AFF_1:33; :: thesis: verum

end;