let S be IncSpace; :: thesis: for L being LINE of S ex K being LINE of S st

for P being PLANE of S holds

( not L on P or not K on P )

let L be LINE of S; :: thesis: ex K being LINE of S st

for P being PLANE of S holds

( not L on P or not K on P )

consider A, B being POINT of S such that

A1: A <> B and

A2: {A,B} on L by Def8;

consider C, D being POINT of S such that

A3: not {A,B,C,D} is planar by A1, Th47;

take K = Line (C,D); :: thesis: for P being PLANE of S holds

( not L on P or not K on P )

given P being PLANE of S such that A4: L on P and

A5: K on P ; :: thesis: contradiction

not {C,D,A,B} is planar by A3, ENUMSET1:73;

then C <> D by Th16;

then {C,D} on K by Def19;

then A6: {C,D} on P by A5, Th14;

{A,B} on P by A2, A4, Th14;

then {A,B} \/ {C,D} on P by A6, Th11;

then {A,B,C,D} on P by ENUMSET1:5;

hence contradiction by A3; :: thesis: verum

for P being PLANE of S holds

( not L on P or not K on P )

let L be LINE of S; :: thesis: ex K being LINE of S st

for P being PLANE of S holds

( not L on P or not K on P )

consider A, B being POINT of S such that

A1: A <> B and

A2: {A,B} on L by Def8;

consider C, D being POINT of S such that

A3: not {A,B,C,D} is planar by A1, Th47;

take K = Line (C,D); :: thesis: for P being PLANE of S holds

( not L on P or not K on P )

given P being PLANE of S such that A4: L on P and

A5: K on P ; :: thesis: contradiction

not {C,D,A,B} is planar by A3, ENUMSET1:73;

then C <> D by Th16;

then {C,D} on K by Def19;

then A6: {C,D} on P by A5, Th14;

{A,B} on P by A2, A4, Th14;

then {A,B} \/ {C,D} on P by A6, Th11;

then {A,B,C,D} on P by ENUMSET1:5;

hence contradiction by A3; :: thesis: verum