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
Plane K,L = Plane L,K
let K, L be LINE of S; ( K <> L & ex A being POINT of S st
( A on K & A on L ) implies Plane K,L = Plane L,K )
assume A1:
K <> L
; ( for A being POINT of S holds
( not A on K or not A on L ) or Plane K,L = Plane L,K )
set P2 = Plane L,K;
set P1 = Plane K,L;
given A being POINT of S such that A2:
A on K
and
A3:
A on L
; Plane K,L = Plane L,K
consider C being POINT of S such that
A4:
A <> C
and
A5:
C on L
by Lm1;
consider B being POINT of S such that
A6:
A <> B
and
A7:
B on K
by Lm1;
A8:
K on Plane L,K
by A1, A2, A3, Def22;
then A9:
B on Plane L,K
by A7, Def17;
A10:
K on Plane K,L
by A1, A2, A3, Def22;
then A11:
B on Plane K,L
by A7, Def17;
A12:
now assume
{A,B,C} is
linear
;
contradictionthen consider L1 being
LINE of
S such that A13:
{A,B,C} on L1
by Def6;
A14:
A on L1
by A13, Th12;
C on L1
by A13, Th12;
then A15:
{A,C} on L1
by A14, Th11;
A16:
{A,B} on K
by A2, A7, Th11;
B on L1
by A13, Th12;
then
{A,B} on L1
by A14, Th11;
then A17:
K = L1
by A6, A16, Def10;
{A,C} on L
by A3, A5, Th11;
hence
contradiction
by A1, A4, A15, A17, Def10;
verum end;
L on Plane L,K
by A1, A2, A3, Def22;
then A18:
C on Plane L,K
by A5, Def17;
A on Plane L,K
by A2, A8, Def17;
then A19:
{A,B,C} on Plane L,K
by A9, A18, Th14;
L on Plane K,L
by A1, A2, A3, Def22;
then A20:
C on Plane K,L
by A5, Def17;
A on Plane K,L
by A2, A10, Def17;
then
{A,B,C} on Plane K,L
by A11, A20, Th14;
hence
Plane K,L = Plane L,K
by A19, A12, Def13; verum