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

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