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: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 ; :: 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:15;
y in Line (y,z) by AFF_1:15;
hence contradiction by A1, A2, A3, A4, AFF_1:21; :: thesis: verum

end;