let S be IncSpace; 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; ( 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 )
; 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
; for Q being PLANE of S holds
( ( K on Q & L on Q ) iff P = Q )
let Q be PLANE of S; ( ( K on Q & L on Q ) iff P = Q )
thus
( K on Q & L on Q implies P = Q )
( 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
;
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;
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; verum