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