let S be IncSpace; :: thesis: for L being LINE of S

for P being PLANE of S ex A being POINT of S st

( A on P & not A on L )

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

( A on P & not A on L )

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

( A on P & not A on L )

consider A, B being POINT of S such that

A1: A <> B and

A2: {A,B} on L by Def8;

consider C being POINT of S such that

A3: C on P and

A4: not {A,B,C} is linear by A1, Th44;

take C ; :: thesis: ( C on P & not C on L )

thus C on P by A3; :: thesis: not C on L

( C on L implies {A,B} \/ {C} on L ) by A2, Th8;

then ( C on L implies {A,B,C} on L ) by ENUMSET1:3;

hence not C on L by A4; :: thesis: verum

for P being PLANE of S ex A being POINT of S st

( A on P & not A on L )

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

( A on P & not A on L )

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

( A on P & not A on L )

consider A, B being POINT of S such that

A1: A <> B and

A2: {A,B} on L by Def8;

consider C being POINT of S such that

A3: C on P and

A4: not {A,B,C} is linear by A1, Th44;

take C ; :: thesis: ( C on P & not C on L )

thus C on P by A3; :: thesis: not C on L

( C on L implies {A,B} \/ {C} on L ) by A2, Th8;

then ( C on L implies {A,B,C} on L ) by ENUMSET1:3;

hence not C on L by A4; :: thesis: verum