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

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