let S be IncSpace; :: thesis: for P being PLANE of S ex A, B, C being POINT of S st
( {A,B,C} on P & not {A,B,C} is linear )
let P be PLANE of S; :: thesis: ex A, B, C being POINT of S st
( {A,B,C} on P & not {A,B,C} is linear )
consider A1, B1, C1, D1 being POINT of S such that
A1: A1 on P and
A2: not {A1,B1,C1,D1} is planar by Lm2;
not {B1,D1,A1,C1} is planar by A2, ENUMSET1:69;
then A3: B1 <> D1 by Th16;
not {C1,D1,A1,B1} is planar by A2, ENUMSET1:73;
then A4: C1 <> D1 by Th16;
not {A1,B1,C1,D1} on P by A2;
then not {B1,C1,D1,A1} on P by ENUMSET1:68;
then not {B1,C1,D1} \/ {A1} on P by ENUMSET1:6;
then not {B1,C1,D1} on P by A1, Th9;
then ( not B1 on P or not C1 on P or not D1 on P ) by Th4;
then consider X being POINT of S such that
A5: ( X = B1 or X = C1 or X = D1 ) and
A6: not X on P ;
not {B1,C1,A1,D1} is planar by A2, ENUMSET1:67;
then B1 <> C1 by Th16;
then consider Y, Z being POINT of S such that
A7: ( ( Y = B1 or Y = C1 or Y = D1 ) & ( Z = B1 or Z = C1 or Z = D1 ) & Y <> X & Z <> X & Y <> Z ) by A5, A3, A4;
set P1 = Plane (X,Y,A1);
set P2 = Plane (X,Z,A1);
A8: now :: thesis: not {A1,X,Y,Z} is planar
assume {A1,X,Y,Z} is planar ; :: thesis: contradiction
then ( {A1,D1,B1,C1} is planar or {A1,D1,C1,B1} is planar ) by A2, A5, A7, ENUMSET1:62;
hence contradiction by A2, ENUMSET1:63, ENUMSET1:64; :: thesis: verum
end;
then not {A1,X,Y} is linear by Th17;
then not {X,Y,A1} is linear by ENUMSET1:59;
then A9: {X,Y,A1} on Plane (X,Y,A1) by Def20;
then A10: A1 on Plane (X,Y,A1) by Th4;
then consider B being POINT of S such that
A11: A1 <> B and
A12: B on Plane (X,Y,A1) and
A13: B on P by A1, Def15;
not {X,Z,A1,Y} is planar by A8, ENUMSET1:69;
then not {X,Z,A1} is linear by Th17;
then A14: {X,Z,A1} on Plane (X,Z,A1) by Def20;
then A15: A1 on Plane (X,Z,A1) by Th4;
then consider C being POINT of S such that
A16: A1 <> C and
A17: C on P and
A18: C on Plane (X,Z,A1) by A1, Def15;
take A1 ; :: thesis: ex B, C being POINT of S st
( {A1,B,C} on P & not {A1,B,C} is linear )
take B ; :: thesis: ex C being POINT of S st
( {A1,B,C} on P & not {A1,B,C} is linear )
take C ; :: thesis: ( {A1,B,C} on P & not {A1,B,C} is linear )
thus {A1,B,C} on P by A1, A13, A17, Th4; :: thesis: not {A1,B,C} is linear
given K being LINE of S such that A19: {A1,B,C} on K ; :: according to INCSP_1:def 6 :: thesis: contradiction
A20: {A1,C} on Plane (X,Z,A1) by A15, A18, Th3;
{A1,C,B} on K by A19, ENUMSET1:57;
then {A1,C} \/ {B} on K by ENUMSET1:3;
then {A1,C} on K by Th10;
then A21: K on Plane (X,Z,A1) by A16, A20, Def14;
consider E being POINT of S such that
A22: B <> E and
A23: E on K by Lm1;
{A1,B} \/ {C} on K by A19, ENUMSET1:3;
then A24: {A1,B} on K by Th10;
A25: now :: thesis: not {X,B,E} is linear
{A1,B} on P by A1, A13, Th3;
then K on P by A11, A24, Def14;
then E on P by A23, Def17;
then A26: {E,B} on P by A13, Th3;
assume {X,B,E} is linear ; :: thesis: contradiction
then consider L being LINE of S such that
A27: {X,B,E} on L ;
A28: X on L by A27, Th2;
{E,B,X} on L by A27, ENUMSET1:60;
then {E,B} \/ {X} on L by ENUMSET1:3;
then {E,B} on L by Th8;
then L on P by A22, A26, Def14;
hence contradiction by A6, A28, Def17; :: thesis: verum
end;
B on K by A19, Th2;
then A29: B on Plane (X,Z,A1) by A21, Def17;
A30: X on Plane (X,Z,A1) by A14, Th4;
A31: X on Plane (X,Y,A1) by A9, Th4;
{A1,B} on Plane (X,Y,A1) by A10, A12, Th3;
then K on Plane (X,Y,A1) by A11, A24, Def14;
then E on Plane (X,Y,A1) by A23, Def17;
then A32: {X,B,E} on Plane (X,Y,A1) by A12, A31, Th4;
E on Plane (X,Z,A1) by A23, A21, Def17;
then {X,B,E} on Plane (X,Z,A1) by A29, A30, Th4;
then Plane (X,Y,A1) = Plane (X,Z,A1) by A25, A32, Def13;
then Z on Plane (X,Y,A1) by A14, Th4;
then {X,Y,A1} \/ {Z} on Plane (X,Y,A1) by A9, Th9;
then {X,Y,A1,Z} on Plane (X,Y,A1) by ENUMSET1:6;
then {X,Y,A1,Z} is planar ;
hence contradiction by A8, ENUMSET1:67; :: thesis: verum