let S be IncSpace; :: thesis: for A, B, C, D being POINT of S st not {A,B,C} is linear & D on Plane (A,B,C) holds

{A,B,C,D} is planar

let A, B, C, D be POINT of S; :: thesis: ( not {A,B,C} is linear & D on Plane (A,B,C) implies {A,B,C,D} is planar )

assume that

A1: not {A,B,C} is linear and

A2: D on Plane (A,B,C) ; :: thesis: {A,B,C,D} is planar

{A,B,C} on Plane (A,B,C) by A1, Def20;

then {A,B,C} \/ {D} on Plane (A,B,C) by A2, Th9;

then {A,B,C,D} on Plane (A,B,C) by ENUMSET1:6;

hence {A,B,C,D} is planar ; :: thesis: verum

{A,B,C,D} is planar

let A, B, C, D be POINT of S; :: thesis: ( not {A,B,C} is linear & D on Plane (A,B,C) implies {A,B,C,D} is planar )

assume that

A1: not {A,B,C} is linear and

A2: D on Plane (A,B,C) ; :: thesis: {A,B,C,D} is planar

{A,B,C} on Plane (A,B,C) by A1, Def20;

then {A,B,C} \/ {D} on Plane (A,B,C) by A2, Th9;

then {A,B,C,D} on Plane (A,B,C) by ENUMSET1:6;

hence {A,B,C,D} is planar ; :: thesis: verum