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 ( not {A,B,C} is linear & D on Plane A,B,C ) ; :: thesis: {A,B,C,D} is planar
then ( {A,B,C} on Plane A,B,C & D on Plane A,B,C ) by Def20;
then {A,B,C} \/ {D} on Plane A,B,C by 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