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

( not K on P or not L on P ) ) holds

K <> L

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

( not K on P or not L on P ) ) implies K <> L )

assume that

A1: for P being PLANE of S holds

( not K on P or not L on P ) and

A2: K = L ; :: thesis: contradiction

consider A, B being POINT of S such that

A3: A <> B and

A4: {A,B} on K by Def8;

A5: ( A on K & B on K ) by A4, Th1;

consider C, D being POINT of S such that

A6: C <> D and

A7: {C,D} on L by Def8;

C on K by A2, A7, Th1;

then {A,B,C} on K by A5, 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

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

( C on Q & D on Q ) by A8, Th5;

then {C,D} on Q by Th3;

then A9: L on Q by A6, A7, Def14;

( A on Q & B on Q ) by A8, Th5;

then {A,B} on Q by Th3;

then K on Q by A3, A4, Def14;

hence contradiction by A1, A9; :: thesis: verum

( not K on P or not L on P ) ) holds

K <> L

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

( not K on P or not L on P ) ) implies K <> L )

assume that

A1: for P being PLANE of S holds

( not K on P or not L on P ) and

A2: K = L ; :: thesis: contradiction

consider A, B being POINT of S such that

A3: A <> B and

A4: {A,B} on K by Def8;

A5: ( A on K & B on K ) by A4, Th1;

consider C, D being POINT of S such that

A6: C <> D and

A7: {C,D} on L by Def8;

C on K by A2, A7, Th1;

then {A,B,C} on K by A5, 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

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

( C on Q & D on Q ) by A8, Th5;

then {C,D} on Q by Th3;

then A9: L on Q by A6, A7, Def14;

( A on Q & B on Q ) by A8, Th5;

then {A,B} on Q by Th3;

then K on Q by A3, A4, Def14;

hence contradiction by A1, A9; :: thesis: verum