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:46;
hence {A,B,C,D} is planar by Def7; :: thesis: verum