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 not {A,B,C} is linear assume
{A,B,C} is
linear
;
contradictionthen consider L1 being
LINE of
S such that A13:
{A,B,C} on L1
;
A14:
A on L1
by A13, Th2;
C on L1
by A13, Th2;
then A15:
{A,C} on L1
by A14, Th1;
A16:
{A,B} on K
by A2, A7, Th1;
B on L1
by A13, Th2;
then
{A,B} on L1
by A14, Th1;
then A17:
K = L1
by A6, A16, Def10;
{A,C} on L
by A3, A5, Th1;
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, Th4;
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, Th4;
hence
Plane (K,L) = Plane (L,K)
by A19, A12, Def13; verum