let S be IncSpace; :: thesis: for A being POINT of S

for P being PLANE of S st A on P holds

ex L, L1, L2 being LINE of S st

( L1 <> L2 & L1 on P & L2 on P & not L on P & A on L & A on L1 & A on L2 )

let A be POINT of S; :: thesis: for P being PLANE of S st A on P holds

ex L, L1, L2 being LINE of S st

( L1 <> L2 & L1 on P & L2 on P & not L on P & A on L & A on L1 & A on L2 )

let P be PLANE of S; :: thesis: ( A on P implies ex L, L1, L2 being LINE of S st

( L1 <> L2 & L1 on P & L2 on P & not L on P & A on L & A on L1 & A on L2 ) )

consider B, C being POINT of S such that

A1: {B,C} on P and

A2: not {A,B,C} is linear by Th46;

consider D being POINT of S such that

A3: not {A,B,C,D} is planar by A2, Th45;

assume A on P ; :: thesis: ex L, L1, L2 being LINE of S st

( L1 <> L2 & L1 on P & L2 on P & not L on P & A on L & A on L1 & A on L2 )

then A4: {A} \/ {B,C} on P by A1, Th9;

then A5: {A,B,C} on P by ENUMSET1:2;

take L3 = Line (A,D); :: thesis: ex L1, L2 being LINE of S st

( L1 <> L2 & L1 on P & L2 on P & not L3 on P & A on L3 & A on L1 & A on L2 )

take L1 = Line (A,B); :: thesis: ex L2 being LINE of S st

( L1 <> L2 & L1 on P & L2 on P & not L3 on P & A on L3 & A on L1 & A on L2 )

take L2 = Line (A,C); :: thesis: ( L1 <> L2 & L1 on P & L2 on P & not L3 on P & A on L3 & A on L1 & A on L2 )

A6: A <> B by A2, Th15;

then A7: {A,B} on L1 by Def19;

A8: not {A,C,B} is linear by A2, ENUMSET1:57;

then A9: A <> C by Th15;

then A10: {A,C} on L2 by Def19;

then ( B on L2 implies {A,C} \/ {B} on L2 ) by Th8;

then ( B on L2 implies {A,C,B} on L2 ) by ENUMSET1:3;

hence L1 <> L2 by A8, A7, Th1; :: thesis: ( L1 on P & L2 on P & not L3 on P & A on L3 & A on L1 & A on L2 )

{A,B} \/ {C} on P by A5, ENUMSET1:3;

then {A,B} on P by Th11;

hence L1 on P by A6, A7, Def14; :: thesis: ( L2 on P & not L3 on P & A on L3 & A on L1 & A on L2 )

{A,C,B} on P by A4, ENUMSET1:2;

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

then {A,C} on P by Th9;

hence L2 on P by A9, A10, Def14; :: thesis: ( not L3 on P & A on L3 & A on L1 & A on L2 )

not {A,D,B,C} is planar by A3, ENUMSET1:63;

then A <> D by Th16;

then A11: {A,D} on L3 by Def19;

then ( L3 on P implies {A,D} on P ) by Th14;

then ( L3 on P implies D on P ) by Th3;

then ( L3 on P implies {A,B,C} \/ {D} on P ) by A5, Th9;

then ( L3 on P implies {A,B,C,D} on P ) by ENUMSET1:6;

hence not L3 on P by A3; :: thesis: ( A on L3 & A on L1 & A on L2 )

thus ( A on L3 & A on L1 & A on L2 ) by A10, A7, A11, Th1; :: thesis: verum

for P being PLANE of S st A on P holds

ex L, L1, L2 being LINE of S st

( L1 <> L2 & L1 on P & L2 on P & not L on P & A on L & A on L1 & A on L2 )

let A be POINT of S; :: thesis: for P being PLANE of S st A on P holds

ex L, L1, L2 being LINE of S st

( L1 <> L2 & L1 on P & L2 on P & not L on P & A on L & A on L1 & A on L2 )

let P be PLANE of S; :: thesis: ( A on P implies ex L, L1, L2 being LINE of S st

( L1 <> L2 & L1 on P & L2 on P & not L on P & A on L & A on L1 & A on L2 ) )

consider B, C being POINT of S such that

A1: {B,C} on P and

A2: not {A,B,C} is linear by Th46;

consider D being POINT of S such that

A3: not {A,B,C,D} is planar by A2, Th45;

assume A on P ; :: thesis: ex L, L1, L2 being LINE of S st

( L1 <> L2 & L1 on P & L2 on P & not L on P & A on L & A on L1 & A on L2 )

then A4: {A} \/ {B,C} on P by A1, Th9;

then A5: {A,B,C} on P by ENUMSET1:2;

take L3 = Line (A,D); :: thesis: ex L1, L2 being LINE of S st

( L1 <> L2 & L1 on P & L2 on P & not L3 on P & A on L3 & A on L1 & A on L2 )

take L1 = Line (A,B); :: thesis: ex L2 being LINE of S st

( L1 <> L2 & L1 on P & L2 on P & not L3 on P & A on L3 & A on L1 & A on L2 )

take L2 = Line (A,C); :: thesis: ( L1 <> L2 & L1 on P & L2 on P & not L3 on P & A on L3 & A on L1 & A on L2 )

A6: A <> B by A2, Th15;

then A7: {A,B} on L1 by Def19;

A8: not {A,C,B} is linear by A2, ENUMSET1:57;

then A9: A <> C by Th15;

then A10: {A,C} on L2 by Def19;

then ( B on L2 implies {A,C} \/ {B} on L2 ) by Th8;

then ( B on L2 implies {A,C,B} on L2 ) by ENUMSET1:3;

hence L1 <> L2 by A8, A7, Th1; :: thesis: ( L1 on P & L2 on P & not L3 on P & A on L3 & A on L1 & A on L2 )

{A,B} \/ {C} on P by A5, ENUMSET1:3;

then {A,B} on P by Th11;

hence L1 on P by A6, A7, Def14; :: thesis: ( L2 on P & not L3 on P & A on L3 & A on L1 & A on L2 )

{A,C,B} on P by A4, ENUMSET1:2;

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

then {A,C} on P by Th9;

hence L2 on P by A9, A10, Def14; :: thesis: ( not L3 on P & A on L3 & A on L1 & A on L2 )

not {A,D,B,C} is planar by A3, ENUMSET1:63;

then A <> D by Th16;

then A11: {A,D} on L3 by Def19;

then ( L3 on P implies {A,D} on P ) by Th14;

then ( L3 on P implies D on P ) by Th3;

then ( L3 on P implies {A,B,C} \/ {D} on P ) by A5, Th9;

then ( L3 on P implies {A,B,C,D} on P ) by ENUMSET1:6;

hence not L3 on P by A3; :: thesis: ( A on L3 & A on L1 & A on L2 )

thus ( A on L3 & A on L1 & A on L2 ) by A10, A7, A11, Th1; :: thesis: verum