let S be IncSpace; :: thesis: for K, L being LINE of S st K <> L & ex A being POINT of S st
( A on K & A on L ) holds
ex P being PLANE of S st
for Q being PLANE of S holds
( ( K on Q & L on Q ) iff P = Q )

let K, L be LINE of S; :: thesis: ( K <> L & ex A being POINT of S st
( A on K & A on L ) implies ex P being PLANE of S st
for Q being PLANE of S holds
( ( K on Q & L on Q ) iff P = Q ) )

assume that
A1: K <> L and
A2: ex A being POINT of S st
( A on K & A on L ) ; :: thesis: ex P being PLANE of S st
for Q being PLANE of S holds
( ( K on Q & L on Q ) iff P = Q )

consider A being POINT of S such that
A3: A on K and
A4: A on L by A2;
consider C being POINT of S such that
A5: A <> C and
A6: C on L by Lm1;
consider B being POINT of S such that
A7: A <> B and
A8: B on K by Lm1;
consider P being PLANE of S such that
A9: {A,B,C} on P by Def12;
A10: A on P by ;
take P ; :: thesis: for Q being PLANE of S holds
( ( K on Q & L on Q ) iff P = Q )

let Q be PLANE of S; :: thesis: ( ( K on Q & L on Q ) iff P = Q )
thus ( K on Q & L on Q implies P = Q ) :: thesis: ( P = Q implies ( K on Q & L on Q ) )
proof
{A,C} on L by A4, A6, Th1;
then not {A,C} on K by ;
then A11: not C on K by ;
assume that
A12: K on Q and
A13: L on Q ; :: thesis: P = Q
A14: C on Q by ;
( A on Q & B on Q ) by A3, A8, A12, Def17;
then A15: {A,B,C} on Q by ;
{A,B} on K by A3, A8, Th1;
then not {A,B,C} is linear by ;
hence P = Q by ; :: thesis: verum
end;
B on P by ;
then A16: {A,B} on P by ;
C on P by ;
then A17: {A,C} on P by ;
A18: {A,C} on L by A4, A6, Th1;
{A,B} on K by A3, A8, Th1;
hence ( P = Q implies ( K on Q & L on Q ) ) by A7, A5, A18, A16, A17, Def14; :: thesis: verum