let S be IncSpace; for K, L being LINE of S st ex A being POINT of S st
( A on K & A on L ) holds
ex P being PLANE of S st
( K on P & L on P )
let K, L be LINE of S; ( ex A being POINT of S st
( A on K & A on L ) implies ex P being PLANE of S st
( K on P & L on P ) )
given A being POINT of S such that A1:
A on K
and
A2:
A on L
; ex P being PLANE of S st
( K on P & L on P )
consider C being POINT of S such that
A3:
A <> C
and
A4:
C on L
by Lm1;
A5:
{A,C} on L
by A2, A4, Th11;
consider B being POINT of S such that
A6:
A <> B
and
A7:
B on K
by Lm1;
consider P being PLANE of S such that
A8:
{A,B,C} on P
by Def12;
take
P
; ( K on P & L on P )
A9:
A on P
by A8, Th14;
C on P
by A8, Th14;
then A10:
{A,C} on P
by A9, Th13;
B on P
by A8, Th14;
then A11:
{A,B} on P
by A9, Th13;
{A,B} on K
by A1, A7, Th11;
hence
( K on P & L on P )
by A6, A3, A5, A11, A10, Def14; verum