let S be IncSpace; :: thesis: for A being POINT of S ex L, L1, L2 being LINE of S st

( A on L & A on L1 & A on L2 & ( for P being PLANE of S holds

( not L on P or not L1 on P or not L2 on P ) ) )

let A be POINT of S; :: thesis: ex L, L1, L2 being LINE of S st

( A on L & A on L1 & A on L2 & ( for P being PLANE of S holds

( not L on P or not L1 on P or not L2 on P ) ) )

consider P being PLANE of S such that

A1: {A,A,A} on P by Def12;

A on P by A1, Th4;

then consider L, L1, L2 being LINE of S such that

A2: L1 <> L2 and

A3: L1 on P and

A4: L2 on P and

A5: not L on P and

A6: A on L and

A7: A on L1 and

A8: A on L2 by Th50;

consider B being POINT of S such that

A9: A <> B and

A10: B on L1 by Lm1;

consider C being POINT of S such that

A11: A <> C and

A12: C on L2 by Lm1;

A13: C on P by A4, A12, Def17;

A14: {A,B} on L1 by A7, A10, Th1;

then {A,B} on P by A3, Th14;

then {A,B} \/ {C} on P by A13, Th9;

then A15: {A,B,C} on P by ENUMSET1:3;

take L ; :: thesis: ex L1, L2 being LINE of S st

( A on L & A on L1 & A on L2 & ( for P being PLANE of S holds

( not L on P or not L1 on P or not L2 on P ) ) )

take L1 ; :: thesis: ex L2 being LINE of S st

( A on L & A on L1 & A on L2 & ( for P being PLANE of S holds

( not L on P or not L1 on P or not L2 on P ) ) )

take L2 ; :: thesis: ( A on L & A on L1 & A on L2 & ( for P being PLANE of S holds

( not L on P or not L1 on P or not L2 on P ) ) )

thus ( A on L & A on L1 & A on L2 ) by A6, A7, A8; :: thesis: for P being PLANE of S holds

( not L on P or not L1 on P or not L2 on P )

given Q being PLANE of S such that A16: L on Q and

A17: L1 on Q and

A18: L2 on Q ; :: thesis: contradiction

A19: C on Q by A18, A12, Def17;

A20: {A,C} on L2 by A8, A12, Th1;

{A,B} on Q by A17, A14, Th14;

then {A,B} \/ {C} on Q by A19, Th9;

then {A,B,C} on Q by ENUMSET1:3;

hence contradiction by A5, A16, A15, A23, Def13; :: thesis: verum

( A on L & A on L1 & A on L2 & ( for P being PLANE of S holds

( not L on P or not L1 on P or not L2 on P ) ) )

let A be POINT of S; :: thesis: ex L, L1, L2 being LINE of S st

( A on L & A on L1 & A on L2 & ( for P being PLANE of S holds

( not L on P or not L1 on P or not L2 on P ) ) )

consider P being PLANE of S such that

A1: {A,A,A} on P by Def12;

A on P by A1, Th4;

then consider L, L1, L2 being LINE of S such that

A2: L1 <> L2 and

A3: L1 on P and

A4: L2 on P and

A5: not L on P and

A6: A on L and

A7: A on L1 and

A8: A on L2 by Th50;

consider B being POINT of S such that

A9: A <> B and

A10: B on L1 by Lm1;

consider C being POINT of S such that

A11: A <> C and

A12: C on L2 by Lm1;

A13: C on P by A4, A12, Def17;

A14: {A,B} on L1 by A7, A10, Th1;

then {A,B} on P by A3, Th14;

then {A,B} \/ {C} on P by A13, Th9;

then A15: {A,B,C} on P by ENUMSET1:3;

take L ; :: thesis: ex L1, L2 being LINE of S st

( A on L & A on L1 & A on L2 & ( for P being PLANE of S holds

( not L on P or not L1 on P or not L2 on P ) ) )

take L1 ; :: thesis: ex L2 being LINE of S st

( A on L & A on L1 & A on L2 & ( for P being PLANE of S holds

( not L on P or not L1 on P or not L2 on P ) ) )

take L2 ; :: thesis: ( A on L & A on L1 & A on L2 & ( for P being PLANE of S holds

( not L on P or not L1 on P or not L2 on P ) ) )

thus ( A on L & A on L1 & A on L2 ) by A6, A7, A8; :: thesis: for P being PLANE of S holds

( not L on P or not L1 on P or not L2 on P )

given Q being PLANE of S such that A16: L on Q and

A17: L1 on Q and

A18: L2 on Q ; :: thesis: contradiction

A19: C on Q by A18, A12, Def17;

A20: {A,C} on L2 by A8, A12, Th1;

now :: thesis: for K being LINE of S holds not {A,B,C} on K

then A23:
not {A,B,C} is linear
;given K being LINE of S such that A21:
{A,B,C} on K
; :: thesis: contradiction

{A,C,B} on K by A21, ENUMSET1:57;

then {A,C} \/ {B} on K by ENUMSET1:3;

then A22: {A,C} on K by Th8;

{A,B} \/ {C} on K by A21, ENUMSET1:3;

then {A,B} on K by Th8;

then K = L1 by A9, A14, Def10;

hence contradiction by A2, A11, A20, A22, Def10; :: thesis: verum

end;{A,C,B} on K by A21, ENUMSET1:57;

then {A,C} \/ {B} on K by ENUMSET1:3;

then A22: {A,C} on K by Th8;

{A,B} \/ {C} on K by A21, ENUMSET1:3;

then {A,B} on K by Th8;

then K = L1 by A9, A14, Def10;

hence contradiction by A2, A11, A20, A22, Def10; :: thesis: verum

{A,B} on Q by A17, A14, Th14;

then {A,B} \/ {C} on Q by A19, Th9;

then {A,B,C} on Q by ENUMSET1:3;

hence contradiction by A5, A16, A15, A23, Def13; :: thesis: verum