let S be IncSpace; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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, Th1;

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 ; :: thesis: ( K on P & L on P )

A9: A on P by A8, Th4;

C on P by A8, Th4;

then A10: {A,C} on P by A9, Th3;

B on P by A8, Th4;

then A11: {A,B} on P by A9, Th3;

{A,B} on K by A1, A7, Th1;

hence ( K on P & L on P ) by A6, A3, A5, A11, A10, Def14; :: thesis: verum

( 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; :: thesis: ( 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 ; :: thesis: 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, Th1;

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 ; :: thesis: ( K on P & L on P )

A9: A on P by A8, Th4;

C on P by A8, Th4;

then A10: {A,C} on P by A9, Th3;

B on P by A8, Th4;

then A11: {A,B} on P by A9, Th3;

{A,B} on K by A1, A7, Th1;

hence ( K on P & L on P ) by A6, A3, A5, A11, A10, Def14; :: thesis: verum