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 Th8;
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 Th11;
assume A5: not {A,B,C,D} is planar ; :: thesis: contradiction
then A <> B by Th16;
then L on P by A2, A4, Def14;
then A6: {A,B,C} on P by A1, Th14;
then A7: C on P by Th4;
A8: D on P by A3, Th4;
( A on P & B on P ) by A6, Th4;
then {A,B,C,D} on P by A7, A8, Th5;
hence contradiction by A5; :: thesis: verum