let S be IncSpace; :: thesis: for L, L1, L2 being LINE of S
for P being PLANE of S st L1 on P & L2 on P & not L on P & L1 <> L2 holds
for Q being PLANE of S holds
( not L on Q or not L1 on Q or not L2 on Q )
let L, L1, L2 be LINE of S; :: thesis: for P being PLANE of S st L1 on P & L2 on P & not L on P & L1 <> L2 holds
for Q being PLANE of S holds
( not L on Q or not L1 on Q or not L2 on Q )
let P be PLANE of S; :: thesis: ( L1 on P & L2 on P & not L on P & L1 <> L2 implies for Q being PLANE of S holds
( not L on Q or not L1 on Q or not L2 on Q ) )
assume that
A1: L1 on P and
A2: L2 on P and
A3: not L on P and
A4: L1 <> L2 ; :: thesis: for Q being PLANE of S holds
( not L on Q or not L1 on Q or not L2 on Q )
consider A, B being POINT of S such that
A5: A <> B and
A6: {A,B} on L1 by Def8;
A7: {A,B} on P by A1, A6, Th14;
consider C, C1 being POINT of S such that
A8: C <> C1 and
A9: {C,C1} on L2 by Def8;
A10: now :: thesis: ( C on L1 implies not C1 on L1 )
assume ( C on L1 & C1 on L1 ) ; :: thesis: contradiction
then {C,C1} on L1 by Th1;
hence contradiction by A4, A8, A9, Def10; :: thesis: verum
end;
A11: {C,C1} on P by A2, A9, Th14;
then C on P by Th3;
then {A,B} \/ {C} on P by A7, Th9;
then A12: {A,B,C} on P by ENUMSET1:3;
C1 on P by A11, Th3;
then {A,B} \/ {C1} on P by A7, Th9;
then A13: {A,B,C1} on P by ENUMSET1:3;
consider D, E being POINT of S such that
A14: D <> E and
A15: {D,E} on L by Def8;
given Q being PLANE of S such that A16: L on Q and
A17: L1 on Q and
A18: L2 on Q ; :: thesis: contradiction
A19: {A,B} on Q by A17, A6, Th14;
A20: {C,C1} on Q by A18, A9, Th14;
then A21: C on Q by Th3;
A22: {D,E} on Q by A16, A15, Th14;
then A23: D on Q by Th3;
then {C,D} on Q by A21, Th3;
then {A,B} \/ {C,D} on Q by A19, Th11;
then {A,B,C,D} on Q by ENUMSET1:5;
then A24: {A,B,C,D} is planar ;
A25: E on Q by A22, Th3;
then {C,E} on Q by A21, Th3;
then {A,B} \/ {C,E} on Q by A19, Th11;
then {A,B,C,E} on Q by ENUMSET1:5;
then A26: {A,B,C,E} is planar ;
A27: C1 on Q by A20, Th3;
then {C1,D} on Q by A23, Th3;
then {A,B} \/ {C1,D} on Q by A19, Th11;
then {A,B,C1,D} on Q by ENUMSET1:5;
then A28: {A,B,C1,D} is planar ;
{C1,E} on Q by A27, A25, Th3;
then {A,B} \/ {C1,E} on Q by A19, Th11;
then {A,B,C1,E} on Q by ENUMSET1:5;
then A29: {A,B,C1,E} is planar ;
not {D,E} on P by A3, A14, A15, Def14;
then ( not D on P or not E on P ) by Th3;
hence contradiction by A5, A6, A24, A26, A28, A29, A10, A12, A13, Th18, Th19; :: thesis: verum