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 & 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 & L on P )
let L be LINE of S; :: thesis: ex P being PLANE of S st
( A on P & L on P )
consider B, C being POINT of S such that
A1: B <> C and
A2: {B,C} on L by Def8;
consider P being PLANE of S such that
A3: {B,C,A} on P by Def12;
take P ; :: thesis: ( A on P & L on P )
thus A on P by A3, Th14; :: thesis: L on P
{B,C} \/ {A} on P by A3, ENUMSET1:43;
then {B,C} on P by Th19;
hence L on P by A1, A2, Def14; :: thesis: verum