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

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