let S be IncSpace; :: thesis: for L being LINE of S ex P, Q being PLANE of S st
( P <> Q & L on P & L on Q )
let L be LINE of S; :: thesis: ex P, Q being PLANE of S st
( P <> Q & L on P & L on Q )
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 P = Plane (A,B,C); :: thesis: ex Q being PLANE of S st
( P <> Q & L on P & L on Q )
take Q = Plane (A,B,D); :: thesis: ( P <> Q & L on P & L on Q )
not {A,B,C} is linear by A3, Th17;
then A4: {A,B,C} on P by Def20;
not {A,B,D,C} is planar by A3, ENUMSET1:61;
then not {A,B,D} is linear by Th17;
then A5: {A,B,D} on Q by Def20;
then {A,B} \/ {D} on Q by ENUMSET1:3;
then A6: {A,B} on Q by Th11;
D on Q by A5, Th4;
then ( P = Q implies {A,B,C} \/ {D} on P ) by A4, Th9;
then ( P = Q implies {A,B,C,D} on P ) by ENUMSET1:6;
hence P <> Q by A3; :: thesis: ( L on P & L on Q )
{A,B} \/ {C} on P by A4, ENUMSET1:3;
then {A,B} on P by Th11;
hence ( L on P & L on Q ) by A1, A2, A6, Def14; :: thesis: verum