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

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