let S be IncSpace; :: thesis: for A, B, C, D being POINT of S st {A,B,C} is linear holds
{A,B,C,D} is planar
let A, B, C, D be POINT of S; :: thesis: ( {A,B,C} is linear implies {A,B,C,D} is planar )
given L being LINE of S such that A1: {A,B,C} on L ; :: according to INCSP_1:def 6 :: thesis: {A,B,C,D} is planar
{A,B} \/ {C} on L by A1, ENUMSET1:3;
then A2: {A,B} on L by Th18;
consider P being PLANE of S such that
A3: {A,B,D} on P by Def12;
{A,B} \/ {D} on P by A3, ENUMSET1:3;
then A4: {A,B} on P by Th21;
assume A5: not {A,B,C,D} is planar ; :: thesis: contradiction
then A <> B by Th37;
then L on P by A2, A4, Def14;
then A6: {A,B,C} on P by A1, Th35;
then A7: C on P by Th14;
A8: D on P by A3, Th14;
( A on P & B on P ) by A6, Th14;
then {A,B,C,D} on P by A7, A8, Th15;
hence contradiction by A5, Def7; :: thesis: verum