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
Plane K,L = Plane L,K
let K, L be LINE of S; :: thesis: ( 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 ; :: thesis: ( for A being POINT of S holds
( not A on K or not A on L ) or Plane K,L = Plane L,K )
given A being POINT of S such that A2: ( A on K & A on L ) ; :: thesis: Plane K,L = Plane L,K
consider B being POINT of S such that
A3: A <> B and
A4: B on K by Lm1;
consider C being POINT of S such that
A5: A <> C and
A6: C on L by Lm1;
set P1 = Plane K,L;
set P2 = Plane L,K;
( K on Plane K,L & L on Plane K,L & K on Plane L,K & L on Plane L,K ) by A1, A2, Def22;
then ( A on Plane K,L & B on Plane K,L & C on Plane K,L & A on Plane L,K & B on Plane L,K & C on Plane L,K ) by A2, A4, A6, Def17;
then A7: ( {A,B,C} on Plane K,L & {A,B,C} on Plane L,K ) by Th14;

now

assume {A,B,C} is linear ; :: thesis: contradiction
then consider L1 being LINE of S such that
A8: {A,B,C} on L1 by Def6;
( A on L1 & B on L1 & C on L1 ) by A8, Th12;
then ( {A,B} on L1 & {A,B} on K & {A,C} on L1 & {A,C} on L ) by A2, A4, A6, Th11;
then ( K = L1 & L = L1 ) by A3, A5, Def10;
hence contradiction by A1; :: thesis: verum

end;

hence Plane K,L = Plane L,K by A7, Def13; :: thesis: verum