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

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 ; :: thesis: 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;

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; :: thesis: verum

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

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 ; :: thesis: 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 :: thesis: not {A,B,C} is linear

L on Plane (L,K)
by A1, A2, A3, Def22;assume
{A,B,C} is linear
; :: thesis: contradiction

then 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; :: thesis: verum

end;then 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; :: thesis: verum

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; :: thesis: verum