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 A9, Th4;
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 A1, A5, Def10;
then A11: not C on K by A3, Th1;
assume that
A12: K on Q and
A13: L on Q ; :: thesis: P = Q
A14: C on Q by A6, A13, Def17;
( A on Q & B on Q ) by A3, A8, A12, Def17;
then A15: {A,B,C} on Q by A14, Th4;
{A,B} on K by A3, A8, Th1;
then not {A,B,C} is linear by A7, A11, Th18;
hence P = Q by A9, A15, Def13; :: thesis: verum

end;

B on P by A9, Th4;
then A16: {A,B} on P by A10, Th3;
C on P by A9, Th4;
then A17: {A,C} on P by A10, Th3;
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