let S be IncSpace; 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; ( 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
; 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
; verum