let S be IncSpace; :: thesis: for A, B, C, D being POINT of S
for P being PLANE of S st not {A,B,C} is linear & {A,B,C} on P & not D on P holds
not {A,B,C,D} is planar
let A, B, C, D be POINT of S; :: thesis: for P being PLANE of S st not {A,B,C} is linear & {A,B,C} on P & not D on P holds
not {A,B,C,D} is planar
let P be PLANE of S; :: thesis: ( not {A,B,C} is linear & {A,B,C} on P & not D on P implies not {A,B,C,D} is planar )
assume that
A1: ( not {A,B,C} is linear & {A,B,C} on P ) and
A2: not D on P ; :: thesis: not {A,B,C,D} is planar
given Q being PLANE of S such that A3: {A,B,C,D} on Q ; :: according to INCSP_1:def 7 :: thesis: contradiction
{A,B,C} \/ {D} on Q by A3, ENUMSET1:6;
then {A,B,C} on Q by Th9;
then P = Q by A1, Def13;
hence contradiction by A2, A3, Th5; :: thesis: verum