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;

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

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;

then A23: not {A,B,C} is linear ;
{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