let S be IncSpace; :: thesis: for L, L1, L2 being LINE of S st ( for P being PLANE of S holds
( not L on P or not L1 on P or not L2 on P ) ) & ex A being POINT of S st
( A on L & A on L1 & A on L2 ) holds
L <> L1
let L, L1, L2 be LINE of S; :: thesis: ( ( for P being PLANE of S holds
( not L on P or not L1 on P or not L2 on P ) ) & ex A being POINT of S st
( A on L & A on L1 & A on L2 ) implies L <> L1 )
assume A1: for P being PLANE of S holds
( not L on P or not L1 on P or not L2 on P ) ; :: thesis: ( for A being POINT of S holds
( not A on L or not A on L1 or not A on L2 ) or L <> L1 )
given A being POINT of S such that A2: A on L and
A3: A on L1 and
A4: A on L2 ; :: thesis: L <> L1
consider C being POINT of S such that
A5: A <> C and
A6: C on L1 by Lm1;
consider D being POINT of S such that
A7: A <> D and
A8: D on L2 by Lm1;
consider B being POINT of S such that
A9: A <> B and
A10: B on L by Lm1;
assume A11: L = L1 ; :: thesis: contradiction
then {A,C,B} on L1 by A3, A10, A6, Th2;
then {A,C} \/ {B} on L1 by ENUMSET1:3;
then A12: {A,C} on L1 by Th10;
{A,B,C} on L by A3, A11, A10, A6, Th2;
then {A,B,C} is linear ;
then {A,B,C,D} is planar by Th17;
then consider Q being PLANE of S such that
A13: {A,B,C,D} on Q ;
( A on Q & D on Q ) by A13, Th5;
then A14: {A,D} on Q by Th3;
{A,D} on L2 by A4, A8, Th1;
then A15: L2 on Q by A7, A14, Def14;
( A on Q & C on Q ) by A13, Th5;
then {A,C} on Q by Th3;
then A16: L1 on Q by A5, A12, Def14;
{A,B} \/ {C,D} on Q by A13, ENUMSET1:5;
then A17: {A,B} on Q by Th11;
{A,B} on L by A2, A10, Th1;
then L on Q by A9, A17, Def14;
hence contradiction by A1, A16, A15; :: thesis: verum