let S be IncSpace; :: thesis: for A, B, C being POINT of S holds {A,A,B,C} is planar
let A, B, C be POINT of S; :: thesis: {A,A,B,C} is planar
consider P being PLANE of S such that
A1: {A,B,C} on P by Def12;
take P ; :: according to INCSP_1:def 7 :: thesis: {A,A,B,C} on P
thus {A,A,B,C} on P by A1, ENUMSET1:31; :: thesis: verum