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, Th11;
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, Th11;
then {A,B,C} on K by A5, Th12;
then {A,B,C} is linear by Def6;
then {A,B,C,D} is planar by Th38;
then consider Q being PLANE of S such that
A8: {A,B,C,D} on Q by Def7;
( C on Q & D on Q ) by A8, Th15;
then {C,D} on Q by Th13;
then A9: L on Q by A6, A7, Def14;
( A on Q & B on Q ) by A8, Th15;
then {A,B} on Q by Th13;
then K on Q by A3, A4, Def14;
hence contradiction by A1, A9; :: thesis: verum