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;

( A on P & not {A,B,C,D} is planar ) by A2; :: thesis: verum

( 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 ) )

hence
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 )

( A on P & not {A,B,C,D} is planar ) by A4; :: thesis: verum

end;( 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 ) )

( 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;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

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 ) )

hence
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;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

( A on P & not {A,B,C,D} is planar ) by A4; :: thesis: verum

( A on P & not {A,B,C,D} is planar ) by A2; :: thesis: verum