let S be IncSpace; :: thesis: for A, B, C being POINT of S st not {A,B,C} is linear holds

ex D being POINT of S st not {A,B,C,D} is planar

let A, B, C be POINT of S; :: thesis: ( not {A,B,C} is linear implies ex D being POINT of S st not {A,B,C,D} is planar )

assume A1: not {A,B,C} is linear ; :: thesis: not for D being POINT of S holds {A,B,C,D} is planar

consider P being PLANE of S such that

A2: {A,B,C} on P by Def12;

consider A1, B1, C1, D1 being POINT of S such that

A3: not {A1,B1,C1,D1} is planar by Def16;

not {A1,B1,C1,D1} on P by A3;

then ( not A1 on P or not B1 on P or not C1 on P or not D1 on P ) by Th5;

then ( not {A,B,C,A1} is planar or not {A,B,C,B1} is planar or not {A,B,C,C1} is planar or not {A,B,C,D1} is planar ) by A1, A2, Th19;

hence not for D being POINT of S holds {A,B,C,D} is planar ; :: thesis: verum

ex D being POINT of S st not {A,B,C,D} is planar

let A, B, C be POINT of S; :: thesis: ( not {A,B,C} is linear implies ex D being POINT of S st not {A,B,C,D} is planar )

assume A1: not {A,B,C} is linear ; :: thesis: not for D being POINT of S holds {A,B,C,D} is planar

consider P being PLANE of S such that

A2: {A,B,C} on P by Def12;

consider A1, B1, C1, D1 being POINT of S such that

A3: not {A1,B1,C1,D1} is planar by Def16;

not {A1,B1,C1,D1} on P by A3;

then ( not A1 on P or not B1 on P or not C1 on P or not D1 on P ) by Th5;

then ( not {A,B,C,A1} is planar or not {A,B,C,B1} is planar or not {A,B,C,C1} is planar or not {A,B,C,D1} is planar ) by A1, A2, Th19;

hence not for D being POINT of S holds {A,B,C,D} is planar ; :: thesis: verum