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 ) )
assume A1: 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 )
consider B, C being POINT of S such that
A2: {B,C} on P and
A3: not {A,B,C} is linear by Th76;
consider D being POINT of S such that
A4: not {A,B,C,D} is planar by A3, Th75;
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 )
A5: not {A,C,B} is linear by A3, ENUMSET1:98;
then A6: A <> C by Th36;
then A7: {A,C} on L2 by Def19;
then ( B on L2 implies {A,C} \/ {B} on L2 ) by Th18;
then A8: ( B on L2 implies {A,C,B} on L2 ) by ENUMSET1:43;
A9: A <> B by A3, Th36;
then A10: {A,B} on L1 by Def19;
hence L1 <> L2 by A5, A8, Def6, Th11; :: thesis: ( L1 on P & L2 on P & not L3 on P & A on L3 & A on L1 & A on L2 )
A11: {A} \/ {B,C} on P by A1, A2, Th19;
then A12: {A,B,C} on P by ENUMSET1:42;
then {A,B} \/ {C} on P by ENUMSET1:43;
then {A,B} on P by Th21;
hence L1 on P by A9, A10, Def14; :: thesis: ( L2 on P & not L3 on P & A on L3 & A on L1 & A on L2 )
{A,C,B} on P by A11, ENUMSET1:42;
then {A,C} \/ {B} on P by ENUMSET1:43;
then {A,C} on P by Th19;
hence L2 on P by A6, A7, Def14; :: thesis: ( not L3 on P & A on L3 & A on L1 & A on L2 )
not {A,D,B,C} is planar by A4, ENUMSET1:105;
then A <> D by Th37;
then A13: {A,D} on L3 by Def19;
then ( L3 on P implies {A,D} on P ) by Th35;
then ( L3 on P implies D on P ) by Th13;
then ( L3 on P implies {A,B,C} \/ {D} on P ) by A12, Th19;
then ( L3 on P implies {A,B,C,D} on P ) by ENUMSET1:46;
hence not L3 on P by A4, Def7; :: thesis: ( A on L3 & A on L1 & A on L2 )
thus ( A on L3 & A on L1 & A on L2 ) by A7, A10, A13, Th11; :: thesis: verum