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;

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

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 )

A11:
{C,C1} on P
by A2, A9, Th14;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;then {C,C1} on L1 by Th1;

hence contradiction by A4, A8, A9, Def10; :: thesis: verum

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