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, Th74;
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, Th18;
then ( C on L implies {A,B,C} on L ) by ENUMSET1:43;
hence not C on L by A4, Def6; :: thesis: verum