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
assume A2: not {A,B,C,D} is planar ; :: thesis: contradiction
consider P being PLANE of S such that
A3: {A,B,D} on P by Def12;
( {A,B} \/ {C} on L & {A,B} \/ {D} on P ) by A1, A3, ENUMSET1:43;
then ( A <> B & {A,B} on L & {A,B} on P ) by A2, Th18, Th21, Th37;
then L on P by Def14;
then {A,B,C} on P by A1, Th35;
then ( A on P & B on P & C on P & D on P ) by A3, Th14;
then {A,B,C,D} on P by Th15;
hence contradiction by A2, Def7; :: thesis: verum