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, Th77;
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,D,C} is planar by A3, ENUMSET1:103;
then ( not {A,B,C} is linear & not {A,B,D} is linear ) by A3, Th38;
then A4: ( {A,B,C} on P & {A,B,D} on Q ) by Def20;
then ( {A,B,C} on P & D on Q ) by Th14;
then ( P = Q implies {A,B,C} \/ {D} on P ) by Th19;
then ( P = Q implies {A,B,C,D} on P ) by ENUMSET1:46;
hence P <> Q by A3, Def7; :: thesis: ( L on P & L on Q )
( {A,B} \/ {C} on P & {A,B} \/ {D} on Q ) by A4, ENUMSET1:43;
then ( {A,B} on P & {A,B} on Q ) by Th21;
hence ( L on P & L on Q ) by A1, A2, Def14; :: thesis: verum