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

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;

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

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

then
not {A1,X,Y} is linear
by Th17;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 ( {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

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

B on K
by A19, Th2;
{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;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

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