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