let S be IncSpace; :: thesis: for A being POINT of S
for P being PLANE of S ex L being LINE of S st
( not A on L & L on P )
let A be POINT of S; :: thesis: for P being PLANE of S ex L being LINE of S st
( not A on L & L on P )
let P be PLANE of S; :: thesis: ex L being LINE of S st
( not A on L & L on P )
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 L being LINE of S such that
A3: {B,C} on L by Def9;
take L ; :: thesis: ( not A on L & L on P )
( A on L implies {B,C} \/ {A} on L ) by A3, Th8;
then ( A on L implies {B,C,A} on L ) by ENUMSET1:3;
then ( A on L implies {A,B,C} on L ) by ENUMSET1:59;
hence not A on L by A2; :: thesis: L on P
not {B,C,A} is linear by A2, ENUMSET1:59;
then B <> C by Th15;
hence L on P by A1, A3, Def14; :: thesis: verum