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, Th19;
then {A,B,C,D} on Plane (A,B,C) by ENUMSET1:6;
hence {A,B,C,D} is planar by Def7; :: thesis: verum