let S be IncSpace; :: thesis: for P being PLANE of S ex A, B, C being POINT of S st
( {A,B,C} on P & not {A,B,C} is linear )
let P be PLANE of S; :: thesis: ex A, B, C being POINT of S st
( {A,B,C} on P & not {A,B,C} is linear )
consider A1, B1, C1, D1 being POINT of S such that
A1: A1 on P and
A2: not {A1,B1,C1,D1} is planar by Lm2;
not {A1,B1,C1,D1} on P by A2, Def7;
then not {B1,C1,D1,A1} on P by ENUMSET1:111;
then not {B1,C1,D1} \/ {A1} on P by ENUMSET1:46;
then not {B1,C1,D1} on P by A1, Th19;
then ( not B1 on P or not C1 on P or not D1 on P ) by Th14;
then consider X being POINT of S such that
A3: ( X = B1 or X = C1 or X = D1 ) and
A4: not X on P ;
( not {B1,C1,A1,D1} is planar & not {B1,D1,A1,C1} is planar & not {C1,D1,A1,B1} is planar ) by A2, ENUMSET1:110, ENUMSET1:112, ENUMSET1:118;
then ( B1 <> C1 & B1 <> D1 & C1 <> D1 ) by Th37;
then consider Y, Z being POINT of S such that
A5: ( ( Y = B1 or Y = C1 or Y = D1 ) & ( Z = B1 or Z = C1 or Z = D1 ) & Y <> X & Z <> X & Y <> Z ) by A3;

A6: now

assume {A1,X,Y,Z} is planar ; :: thesis: contradiction
then ( {A1,D1,B1,C1} is planar or {A1,D1,C1,B1} is planar ) by A2, A3, A5, ENUMSET1:104;
hence contradiction by A2, ENUMSET1:105, ENUMSET1:107; :: thesis: verum

end;

set P1 = Plane X,Y,A1;
set P2 = Plane X,Z,A1;
not {A1,X,Y} is linear by A6, Th38;
then not {X,Y,A1} is linear by ENUMSET1:100;
then A7: {X,Y,A1} on Plane X,Y,A1 by Def20;
then A8: A1 on Plane X,Y,A1 by Th14;
then consider B being POINT of S such that
A9: A1 <> B and
A10: B on Plane X,Y,A1 and
A11: B on P by A1, Def15;
not {X,Z,A1,Y} is planar by A6, ENUMSET1:112;
then not {X,Z,A1} is linear by Th38;
then A12: {X,Z,A1} on Plane X,Z,A1 by Def20;
then A13: A1 on Plane X,Z,A1 by Th14;
then consider C being POINT of S such that
A14: A1 <> C and
A15: C on P and
A16: C on Plane X,Z,A1 by A1, Def15;
take A1 ; :: thesis: ex B, C being POINT of S st
( {A1,B,C} on P & not {A1,B,C} is linear )
take B ; :: thesis: ex C being POINT of S st
( {A1,B,C} on P & not {A1,B,C} is linear )
take C ; :: thesis: ( {A1,B,C} on P & not {A1,B,C} is linear )
thus {A1,B,C} on P by A1, A11, A15, Th14; :: thesis: not {A1,B,C} is linear
given K being LINE of S such that A17: {A1,B,C} on K ; :: according to INCSP_1:def 6 :: thesis: contradiction
A18: B on K by A17, Th12;
consider E being POINT of S such that
A19: B <> E and
A20: E on K by Lm1;
{A1,C,B} on K by A17, ENUMSET1:98;
then ( {A1,B} \/ {C} on K & {A1,C} \/ {B} on K ) by A17, ENUMSET1:43;
then A21: ( {A1,B} on K & {A1,C} on K & {A1,B} on Plane X,Y,A1 & {A1,C} on Plane X,Z,A1 ) by A8, A10, A13, A16, Th13, Th20;
then ( K on Plane X,Y,A1 & K on Plane X,Z,A1 ) by A9, A14, Def14;
then A22: ( B on Plane X,Z,A1 & E on Plane X,Y,A1 & E on Plane X,Z,A1 ) by A18, A20, Def17;

A23: now

assume {X,B,E} is linear ; :: thesis: contradiction
then consider L being LINE of S such that
A24: {X,B,E} on L by Def6;
A25: {E,B,X} on L by A24, ENUMSET1:102;
{A1,B} on P by A1, A11, Th13;
then K on P by A9, A21, Def14;
then ( E on P & {E,B} \/ {X} on L ) by A20, A25, Def17, ENUMSET1:43;
then ( {E,B} on P & {E,B} on L ) by A11, Th13, Th18;
then ( L on P & X on L ) by A19, A24, Def14, Th12;
hence contradiction by A4, Def17; :: thesis: verum

end;

( X on Plane X,Y,A1 & X on Plane X,Z,A1 ) by A7, A12, Th14;
then ( {X,B,E} on Plane X,Y,A1 & {X,B,E} on Plane X,Z,A1 ) by A10, A22, Th14;
then Plane X,Y,A1 = Plane X,Z,A1 by A23, Def13;
then Z on Plane X,Y,A1 by A12, Th14;
then {X,Y,A1} \/ {Z} on Plane X,Y,A1 by A7, Th19;
then {X,Y,A1,Z} on Plane X,Y,A1 by ENUMSET1:46;
then {X,Y,A1,Z} is planar by Def7;
hence contradiction by A6, ENUMSET1:110; :: thesis: verum