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