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

{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