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