let S be IncSpace; 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; 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 ( 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
;
ex A, B, C, D being POINT of S st
( A on P & not {A,B,C,D} is planar )A4:
now ( 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)
;
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;
verum end; now ( 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)
;
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;
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;
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; verum