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 ;
then A6: {A1,B1} on Line (A1,B1) by Def19;
{A1,B1} on Line (A1,B1) by ;
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 ;
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 ;
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 ;
then {A1,B1} on Plane (A1,B1,C1) by Th11;
then Line (A1,B1) on Plane (A1,B1,C1) by ;
then A on Plane (A1,B1,C1) by ;
then A13: {A,A1,C1} on Plane (A1,B1,C1) by ;
A1 on Line (A1,B1) by ;
then {A,A1} on Line (A1,B1) by ;
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 ;
then A16: {A1,B1} on Line (A1,B1) by Def19;
then not {A1,B1,A} is linear by ;
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 ;
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