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;
reconsider a = x as POINT of (IncProjSp_of AS) by Th20;
reconsider A = [(Line y,z),1] as LINE of (IncProjSp_of AS) by A2, Th23;
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;
( y in Line y,z & z in Line y,z ) by AFF_1:26;
hence contradiction by A1, A2, A3, AFF_1:33; :: thesis: verum

end;