let S be IncSpace; :: thesis: for P being PLANE of S ex A, B, C, D being POINT of S st
( A on P & not {A,B,C,D} is planar )
let P be PLANE of S; :: thesis: ex A, B, C, D being POINT of S st
( A on P & not {A,B,C,D} is planar )
consider A being POINT of S such that
A1: A on P by Def11;
consider A1, B1, C1, D1 being POINT of S such that
A2: not {A1,B1,C1,D1} is planar by Def16;

now

assume A3: not A1 on P ; :: thesis: ex A, B, C, D being POINT of S st
( A on P & not {A,B,C,D} is planar )

A4: now

assume A5: A on Line A1,B1 ; :: thesis: ex A, B, C, D being POINT of S st
( A on P & not {A,B,C,D} is planar )
set Q = Plane A1,B1,C1;
A6: A1 <> B1 by A2, Th37;
then A7: {A1,B1} on Line A1,B1 by Def19;
then A1 on Line A1,B1 by Th11;
then A8: {A,A1} on Line A1,B1 by A5, Th11;
A9: not {A1,B1,C1} is linear by A2, Th38;
then A10: {A1,B1,C1} on Plane A1,B1,C1 by Def20;
then ( D1 on Plane A1,B1,C1 implies {A1,B1,C1} \/ {D1} on Plane A1,B1,C1 ) by Th19;
then A11: ( D1 on Plane A1,B1,C1 implies {A1,B1,C1,D1} on Plane A1,B1,C1 ) by ENUMSET1:46;
{A1,B1} on Line A1,B1 by A6, Def19;
then ( C1 on Line A1,B1 implies {A1,B1} \/ {C1} on Line A1,B1 ) by Th18;
then ( C1 on Line A1,B1 implies {A1,B1,C1} on Line A1,B1 ) by ENUMSET1:43;
then A12: not {A,A1,C1} is linear by A1, A3, A8, A9, Def6, Th39;
{A1,B1} \/ {C1} on Plane A1,B1,C1 by A10, ENUMSET1:43;
then {A1,B1} on Plane A1,B1,C1 by Th21;
then ( Line A1,B1 on Plane A1,B1,C1 & {A1,B1,C1} on Plane A1,B1,C1 ) by A6, A7, A9, Def14, Def20;
then ( A on Plane A1,B1,C1 & A1 on Plane A1,B1,C1 & C1 on Plane A1,B1,C1 ) by A5, Def17, Th14;
then {A,A1,C1} on Plane A1,B1,C1 by Th14;
then not {A,A1,C1,D1} is planar by A2, A11, A12, Def7, Th40;
hence ex A, B, C, D being POINT of S st
( A on P & not {A,B,C,D} is planar ) by A1; :: thesis: verum

end;

now

assume A13: not A on Line A1,B1 ; :: thesis: ex A, B, C, D being POINT of S st
( A on P & not {A,B,C,D} is planar )
set Q = Plane A1,B1,A;
A14: A1 <> B1 by A2, Th37;
then A15: {A1,B1} on Line A1,B1 by Def19;
then not {A1,B1,A} is linear by A13, A14, Th39;
then A16: {A1,B1,A} on Plane A1,B1,A by Def20;
then {A1,B1} \/ {A} on Plane A1,B1,A by ENUMSET1:43;
then {A1,B1} on Plane A1,B1,A by Th19;
then ( {C1,D1} on Plane A1,B1,A implies {A1,B1} \/ {C1,D1} on Plane A1,B1,A ) by Th21;
then ( {C1,D1} on Plane A1,B1,A implies {A1,B1,C1,D1} on Plane A1,B1,A ) by ENUMSET1:45;
then ( not C1 on Plane A1,B1,A or not D1 on Plane A1,B1,A ) by A2, Def7, Th13;
then ( not {A1,B1,A,C1} is planar or not {A1,B1,A,D1} is planar ) by A13, A14, A15, A16, Th39, Th40;
then ( not {A,A1,B1,C1} is planar or not {A,A1,B1,D1} is planar ) by ENUMSET1:110;
hence ex A, B, C, D being POINT of S st
( A on P & not {A,B,C,D} is planar ) by A1; :: thesis: verum

end;

hence ex A, B, C, D being POINT of S st
( A on P & not {A,B,C,D} is planar ) by A4; :: thesis: verum

end;

hence ex A, B, C, D being POINT of S st
( A on P & not {A,B,C,D} is planar ) by A2; :: thesis: verum