let S be IncSpace; :: thesis: for A, B being POINT of S holds {A,A,B} is linear
let A, B be POINT of S; :: thesis: {A,A,B} is linear
consider K being LINE of S such that
A1: {A,B} on K by Def9;
take K ; :: according to INCSP_1:def 6 :: thesis: {A,A,B} on K
thus {A,A,B} on K by A1, ENUMSET1:30; :: thesis: verum