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

for L being LINE of S ex P being PLANE of S st

( A on P & not L on P )

let A be POINT of S; :: thesis: for L being LINE of S ex P being PLANE of S st

( A on P & not L on P )

let L be LINE of S; :: thesis: ex P being PLANE of S st

( A on P & not L on P )

consider B being POINT of S such that

A1: A <> B and

A2: B on L by Lm1;

consider C, D being POINT of S such that

A3: not {A,B,C,D} is planar by A1, Th47;

take P = Plane (A,C,D); :: thesis: ( A on P & not L on P )

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

then not {A,C,D} is linear by Th17;

then A5: {A,C,D} on P by Def20;

hence A on P by Th4; :: thesis: not L on P

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

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

hence not L on P by A2, A4, Def17; :: thesis: verum

for L being LINE of S ex P being PLANE of S st

( A on P & not L on P )

let A be POINT of S; :: thesis: for L being LINE of S ex P being PLANE of S st

( A on P & not L on P )

let L be LINE of S; :: thesis: ex P being PLANE of S st

( A on P & not L on P )

consider B being POINT of S such that

A1: A <> B and

A2: B on L by Lm1;

consider C, D being POINT of S such that

A3: not {A,B,C,D} is planar by A1, Th47;

take P = Plane (A,C,D); :: thesis: ( A on P & not L on P )

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

then not {A,C,D} is linear by Th17;

then A5: {A,C,D} on P by Def20;

hence A on P by Th4; :: thesis: not L on P

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

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

hence not L on P by A2, A4, Def17; :: thesis: verum