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 :: thesis: ( not A1 on P implies ex A, B, C, D being POINT of S st
( A on P & not {A,B,C,D} is planar ) )

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 :: thesis: ( A on Line (A1,B1) implies ex A, B, C, D being POINT of S st
( A on P & not {A,B,C,D} is planar ) )

A5: A1 <> B1 by A2, Th16;
then A6: {A1,B1} on Line (A1,B1) by Def19;
{A1,B1} on Line (A1,B1) by A5, Def19;
then ( C1 on Line (A1,B1) implies {A1,B1} \/ {C1} on Line (A1,B1) ) by Th8;
then A7: ( C1 on Line (A1,B1) implies {A1,B1,C1} on Line (A1,B1) ) by ENUMSET1:3;
set Q = Plane (A1,B1,C1);
assume A8: 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 )
A9: not {A1,B1,C1} is linear by A2, Th17;
then {A1,B1,C1} on Plane (A1,B1,C1) by Def20;
then A10: ( A1 on Plane (A1,B1,C1) & C1 on Plane (A1,B1,C1) ) by Th4;
A11: {A1,B1,C1} on Plane (A1,B1,C1) by A9, Def20;
then ( D1 on Plane (A1,B1,C1) implies {A1,B1,C1} \/ {D1} on Plane (A1,B1,C1) ) by Th9;
then A12: ( D1 on Plane (A1,B1,C1) implies {A1,B1,C1,D1} on Plane (A1,B1,C1) ) by ENUMSET1:6;
{A1,B1} \/ {C1} on Plane (A1,B1,C1) by A11, ENUMSET1:3;
then {A1,B1} on Plane (A1,B1,C1) by Th11;
then Line (A1,B1) on Plane (A1,B1,C1) by A5, A6, Def14;
then A on Plane (A1,B1,C1) by A8, Def17;
then A13: {A,A1,C1} on Plane (A1,B1,C1) by A10, Th4;
A1 on Line (A1,B1) by A6, Th1;
then {A,A1} on Line (A1,B1) by A8, Th1;
then not {A,A1,C1} is linear by A1, A3, A9, A7, Th18;
then not {A,A1,C1,D1} is planar by A2, A12, A13, Th19;
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 :: thesis: ( not A on Line (A1,B1) implies 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);
assume A14: 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 )
A15: A1 <> B1 by A2, Th16;
then A16: {A1,B1} on Line (A1,B1) by Def19;
then not {A1,B1,A} is linear by A14, A15, Th18;
then A17: {A1,B1,A} on Plane (A1,B1,A) by Def20;
then {A1,B1} \/ {A} on Plane (A1,B1,A) by ENUMSET1:3;
then {A1,B1} on Plane (A1,B1,A) by Th9;
then ( {C1,D1} on Plane (A1,B1,A) implies {A1,B1} \/ {C1,D1} on Plane (A1,B1,A) ) by Th11;
then ( {C1,D1} on Plane (A1,B1,A) implies {A1,B1,C1,D1} on Plane (A1,B1,A) ) by ENUMSET1:5;
then ( not C1 on Plane (A1,B1,A) or not D1 on Plane (A1,B1,A) ) by A2, Th3;
then ( not {A1,B1,A,C1} is planar or not {A1,B1,A,D1} is planar ) by A14, A15, A16, A17, Th18, Th19;
then ( not {A,A1,B1,C1} is planar or not {A,A1,B1,D1} is planar ) by ENUMSET1:67;
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