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