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

( 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