let S be IncSpace; :: thesis: for L, L1, L2 being LINE of S st ( for P being PLANE of S holds

( not L on P or not L1 on P or not L2 on P ) ) & ex A being POINT of S st

( A on L & A on L1 & A on L2 ) holds

L <> L1

let L, L1, L2 be LINE of S; :: thesis: ( ( for P being PLANE of S holds

( not L on P or not L1 on P or not L2 on P ) ) & ex A being POINT of S st

( A on L & A on L1 & A on L2 ) implies L <> L1 )

assume A1: for P being PLANE of S holds

( not L on P or not L1 on P or not L2 on P ) ; :: thesis: ( for A being POINT of S holds

( not A on L or not A on L1 or not A on L2 ) or L <> L1 )

given A being POINT of S such that A2: A on L and

A3: A on L1 and

A4: A on L2 ; :: thesis: L <> L1

consider C being POINT of S such that

A5: A <> C and

A6: C on L1 by Lm1;

consider D being POINT of S such that

A7: A <> D and

A8: D on L2 by Lm1;

consider B being POINT of S such that

A9: A <> B and

A10: B on L by Lm1;

assume A11: L = L1 ; :: thesis: contradiction

then {A,C,B} on L1 by A3, A10, A6, Th2;

then {A,C} \/ {B} on L1 by ENUMSET1:3;

then A12: {A,C} on L1 by Th10;

{A,B,C} on L by A3, A11, A10, A6, Th2;

then {A,B,C} is linear ;

then {A,B,C,D} is planar by Th17;

then consider Q being PLANE of S such that

A13: {A,B,C,D} on Q ;

( A on Q & D on Q ) by A13, Th5;

then A14: {A,D} on Q by Th3;

{A,D} on L2 by A4, A8, Th1;

then A15: L2 on Q by A7, A14, Def14;

( A on Q & C on Q ) by A13, Th5;

then {A,C} on Q by Th3;

then A16: L1 on Q by A5, A12, Def14;

{A,B} \/ {C,D} on Q by A13, ENUMSET1:5;

then A17: {A,B} on Q by Th11;

{A,B} on L by A2, A10, Th1;

then L on Q by A9, A17, Def14;

hence contradiction by A1, A16, A15; :: thesis: verum

( not L on P or not L1 on P or not L2 on P ) ) & ex A being POINT of S st

( A on L & A on L1 & A on L2 ) holds

L <> L1

let L, L1, L2 be LINE of S; :: thesis: ( ( for P being PLANE of S holds

( not L on P or not L1 on P or not L2 on P ) ) & ex A being POINT of S st

( A on L & A on L1 & A on L2 ) implies L <> L1 )

assume A1: for P being PLANE of S holds

( not L on P or not L1 on P or not L2 on P ) ; :: thesis: ( for A being POINT of S holds

( not A on L or not A on L1 or not A on L2 ) or L <> L1 )

given A being POINT of S such that A2: A on L and

A3: A on L1 and

A4: A on L2 ; :: thesis: L <> L1

consider C being POINT of S such that

A5: A <> C and

A6: C on L1 by Lm1;

consider D being POINT of S such that

A7: A <> D and

A8: D on L2 by Lm1;

consider B being POINT of S such that

A9: A <> B and

A10: B on L by Lm1;

assume A11: L = L1 ; :: thesis: contradiction

then {A,C,B} on L1 by A3, A10, A6, Th2;

then {A,C} \/ {B} on L1 by ENUMSET1:3;

then A12: {A,C} on L1 by Th10;

{A,B,C} on L by A3, A11, A10, A6, Th2;

then {A,B,C} is linear ;

then {A,B,C,D} is planar by Th17;

then consider Q being PLANE of S such that

A13: {A,B,C,D} on Q ;

( A on Q & D on Q ) by A13, Th5;

then A14: {A,D} on Q by Th3;

{A,D} on L2 by A4, A8, Th1;

then A15: L2 on Q by A7, A14, Def14;

( A on Q & C on Q ) by A13, Th5;

then {A,C} on Q by Th3;

then A16: L1 on Q by A5, A12, Def14;

{A,B} \/ {C,D} on Q by A13, ENUMSET1:5;

then A17: {A,B} on Q by Th11;

{A,B} on L by A2, A10, Th1;

then L on Q by A9, A17, Def14;

hence contradiction by A1, A16, A15; :: thesis: verum