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 ) )

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

( 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

B on P
by A9, Th4;
{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;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

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