:: Special Polygons :: by Czes\law Byli\'nski and Yatsuka Nakamura :: :: Received January 30, 1995 :: Copyright (c) 1995-2012 Association of Mizar Users begin theorem :: SPPOL_2:1 for r1, r2, r19, r29 being real number st |[r1,r2]| = |[r19,r29]| holds ( r1 = r19 & r2 = r29 ) by FINSEQ_1:77; theorem Th2: :: SPPOL_2:2 for f being FinSequence of (TOP-REAL 2) for i, j being Nat st i + j = len f holds LSeg (f,i) = LSeg ((Rev f),j) proofend; theorem Th3: :: SPPOL_2:3 for f being FinSequence of (TOP-REAL 2) for i, n being Nat st i + 1 <= len (f | n) holds LSeg ((f | n),i) = LSeg (f,i) proofend; theorem Th4: :: SPPOL_2:4 for f being FinSequence of (TOP-REAL 2) for i, n being Nat st n <= len f & 1 <= i holds LSeg ((f /^ n),i) = LSeg (f,(n + i)) proofend; theorem Th5: :: SPPOL_2:5 for f being FinSequence of (TOP-REAL 2) for i, n being Nat st 1 <= i & i + 1 <= (len f) - n holds LSeg ((f /^ n),i) = LSeg (f,(n + i)) proofend; theorem Th6: :: SPPOL_2:6 for f, g being FinSequence of (TOP-REAL 2) for i being Nat st i + 1 <= len f holds LSeg ((f ^ g),i) = LSeg (f,i) proofend; theorem Th7: :: SPPOL_2:7 for f, g being FinSequence of (TOP-REAL 2) for i being Nat st 1 <= i holds LSeg ((f ^ g),((len f) + i)) = LSeg (g,i) proofend; theorem Th8: :: SPPOL_2:8 for f, g being FinSequence of (TOP-REAL 2) st not f is empty & not g is empty holds LSeg ((f ^ g),(len f)) = LSeg ((f /. (len f)),(g /. 1)) proofend; theorem Th9: :: SPPOL_2:9 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) for i being Nat st i + 1 <= len (f -: p) holds LSeg ((f -: p),i) = LSeg (f,i) proofend; theorem Th10: :: SPPOL_2:10 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) for i being Nat st p in rng f holds LSeg ((f :- p),(i + 1)) = LSeg (f,(i + (p .. f))) proofend; theorem Th11: :: SPPOL_2:11 L~ (<*> the carrier of (TOP-REAL 2)) = {} by TOPREAL1:22; theorem Th12: :: SPPOL_2:12 for p being Point of (TOP-REAL 2) holds L~ <*p*> = {} proofend; theorem Th13: :: SPPOL_2:13 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st p in L~ f holds ex i being Element of NAT st ( 1 <= i & i + 1 <= len f & p in LSeg (f,i) ) proofend; theorem Th14: :: SPPOL_2:14 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st p in L~ f holds ex i being Element of NAT st ( 1 <= i & i + 1 <= len f & p in LSeg ((f /. i),(f /. (i + 1))) ) proofend; theorem Th15: :: SPPOL_2:15 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) for i being Element of NAT st 1 <= i & i + 1 <= len f & p in LSeg ((f /. i),(f /. (i + 1))) holds p in L~ f proofend; theorem :: SPPOL_2:16 for f being FinSequence of (TOP-REAL 2) for i being Element of NAT st 1 <= i & i + 1 <= len f holds LSeg ((f /. i),(f /. (i + 1))) c= L~ f proofend; theorem :: SPPOL_2:17 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) for i being Element of NAT st p in LSeg (f,i) holds p in L~ f proofend; theorem Th18: :: SPPOL_2:18 for f being FinSequence of (TOP-REAL 2) st len f >= 2 holds rng f c= L~ f proofend; theorem Th19: :: SPPOL_2:19 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st not f is empty holds L~ (f ^ <*p*>) = (L~ f) \/ (LSeg ((f /. (len f)),p)) proofend; theorem Th20: :: SPPOL_2:20 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st not f is empty holds L~ (<*p*> ^ f) = (LSeg (p,(f /. 1))) \/ (L~ f) proofend; theorem Th21: :: SPPOL_2:21 for p, q being Point of (TOP-REAL 2) holds L~ <*p,q*> = LSeg (p,q) proofend; theorem Th22: :: SPPOL_2:22 for f being FinSequence of (TOP-REAL 2) holds L~ f = L~ (Rev f) proofend; theorem Th23: :: SPPOL_2:23 for f1, f2 being FinSequence of (TOP-REAL 2) st not f1 is empty & not f2 is empty holds L~ (f1 ^ f2) = ((L~ f1) \/ (LSeg ((f1 /. (len f1)),(f2 /. 1)))) \/ (L~ f2) proofend; Lm1: for f being FinSequence of (TOP-REAL 2) for n being Element of NAT holds L~ (f | n) c= L~ f proofend; theorem Th24: :: SPPOL_2:24 for f being FinSequence of (TOP-REAL 2) for q being Point of (TOP-REAL 2) st q in rng f holds L~ f = (L~ (f -: q)) \/ (L~ (f :- q)) proofend; theorem Th25: :: SPPOL_2:25 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) for n being Element of NAT st p in LSeg (f,n) holds L~ f = L~ (Ins (f,n,p)) proofend; begin registration clusterV15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like being_S-Seq for FinSequence of the carrier of (TOP-REAL 2); existence ex b1 being FinSequence of (TOP-REAL 2) st b1 is being_S-Seq proofend; cluster being_S-Seq -> non trivial one-to-one special unfolded s.n.c. for FinSequence of the carrier of (TOP-REAL 2); coherence for b1 being FinSequence of (TOP-REAL 2) st b1 is being_S-Seq holds ( b1 is one-to-one & b1 is unfolded & b1 is s.n.c. & b1 is special & not b1 is trivial ) proofend; cluster non trivial one-to-one special unfolded s.n.c. -> being_S-Seq for FinSequence of the carrier of (TOP-REAL 2); coherence for b1 being FinSequence of (TOP-REAL 2) st b1 is one-to-one & b1 is unfolded & b1 is s.n.c. & b1 is special & not b1 is trivial holds b1 is being_S-Seq proofend; cluster being_S-Seq -> non empty for FinSequence of the carrier of (TOP-REAL 2); coherence for b1 being FinSequence of (TOP-REAL 2) st b1 is being_S-Seq holds not b1 is empty by CARD_1:27, TOPREAL1:def_8; end; registration cluster non trivial V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like one-to-one V32() FinSequence-like FinSubsequence-like special unfolded s.n.c. for FinSequence of the carrier of (TOP-REAL 2); existence ex b1 being FinSequence of (TOP-REAL 2) st ( b1 is one-to-one & b1 is unfolded & b1 is s.n.c. & b1 is special & not b1 is trivial ) proofend; end; theorem Th26: :: SPPOL_2:26 for f being FinSequence of (TOP-REAL 2) st len f <= 2 holds f is unfolded proofend; Lm2: for p, q being Point of (TOP-REAL 2) holds <*p,q*> is unfolded proofend; Lm3: for f being FinSequence of (TOP-REAL 2) for n being Element of NAT st f is unfolded holds f | n is unfolded proofend; Lm4: for f being FinSequence of (TOP-REAL 2) for n being Element of NAT st f is unfolded holds f /^ n is unfolded proofend; registration let f be unfolded FinSequence of (TOP-REAL 2); let n be Element of NAT ; clusterf | n -> unfolded for FinSequence of (TOP-REAL 2); coherence for b1 being FinSequence of (TOP-REAL 2) st b1 = f | n holds b1 is unfolded by Lm3; clusterf /^ n -> unfolded for FinSequence of (TOP-REAL 2); coherence for b1 being FinSequence of (TOP-REAL 2) st b1 = f /^ n holds b1 is unfolded by Lm4; end; theorem Th27: :: SPPOL_2:27 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st p in rng f & f is unfolded holds f :- p is unfolded proofend; Lm5: for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st f is unfolded holds f -: p is unfolded proofend; registration let f be unfolded FinSequence of (TOP-REAL 2); let p be Point of (TOP-REAL 2); clusterf -: p -> unfolded ; coherence f -: p is unfolded by Lm5; end; theorem Th28: :: SPPOL_2:28 for f being FinSequence of (TOP-REAL 2) st f is unfolded holds Rev f is unfolded proofend; theorem Th29: :: SPPOL_2:29 for g being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st g is unfolded & (LSeg (p,(g /. 1))) /\ (LSeg (g,1)) = {(g /. 1)} holds <*p*> ^ g is unfolded proofend; theorem Th30: :: SPPOL_2:30 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) for k being Element of NAT st f is unfolded & k + 1 = len f & (LSeg (f,k)) /\ (LSeg ((f /. (len f)),p)) = {(f /. (len f))} holds f ^ <*p*> is unfolded proofend; theorem Th31: :: SPPOL_2:31 for f, g being FinSequence of (TOP-REAL 2) for k being Element of NAT st f is unfolded & g is unfolded & k + 1 = len f & (LSeg (f,k)) /\ (LSeg ((f /. (len f)),(g /. 1))) = {(f /. (len f))} & (LSeg ((f /. (len f)),(g /. 1))) /\ (LSeg (g,1)) = {(g /. 1)} holds f ^ g is unfolded proofend; theorem Th32: :: SPPOL_2:32 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) for n being Element of NAT st f is unfolded & p in LSeg (f,n) holds Ins (f,n,p) is unfolded proofend; theorem Th33: :: SPPOL_2:33 for f being FinSequence of (TOP-REAL 2) st len f <= 2 holds f is s.n.c. proofend; Lm6: for p, q being Point of (TOP-REAL 2) holds <*p,q*> is s.n.c. proofend; Lm7: for f being FinSequence of (TOP-REAL 2) for n being Element of NAT st f is s.n.c. holds f | n is s.n.c. proofend; Lm8: for f being FinSequence of (TOP-REAL 2) for n being Element of NAT st f is s.n.c. holds f /^ n is s.n.c. proofend; registration let f be s.n.c. FinSequence of (TOP-REAL 2); let n be Element of NAT ; clusterf | n -> s.n.c. for FinSequence of (TOP-REAL 2); coherence for b1 being FinSequence of (TOP-REAL 2) st b1 = f | n holds b1 is s.n.c. by Lm7; clusterf /^ n -> s.n.c. for FinSequence of (TOP-REAL 2); coherence for b1 being FinSequence of (TOP-REAL 2) st b1 = f /^ n holds b1 is s.n.c. by Lm8; end; Lm9: for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st f is s.n.c. holds f -: p is s.n.c. proofend; registration let f be s.n.c. FinSequence of (TOP-REAL 2); let p be Point of (TOP-REAL 2); clusterf -: p -> s.n.c. ; coherence f -: p is s.n.c. by Lm9; end; theorem Th34: :: SPPOL_2:34 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st p in rng f & f is s.n.c. holds f :- p is s.n.c. proofend; theorem Th35: :: SPPOL_2:35 for f being FinSequence of (TOP-REAL 2) st f is s.n.c. holds Rev f is s.n.c. proofend; theorem Th36: :: SPPOL_2:36 for f, g being FinSequence of (TOP-REAL 2) st f is s.n.c. & g is s.n.c. & L~ f misses L~ g & ( for i being Element of NAT st 1 <= i & i + 2 <= len f holds LSeg (f,i) misses LSeg ((f /. (len f)),(g /. 1)) ) & ( for i being Element of NAT st 2 <= i & i + 1 <= len g holds LSeg (g,i) misses LSeg ((f /. (len f)),(g /. 1)) ) holds f ^ g is s.n.c. proofend; theorem Th37: :: SPPOL_2:37 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) for n being Element of NAT st f is unfolded & f is s.n.c. & p in LSeg (f,n) & not p in rng f holds Ins (f,n,p) is s.n.c. proofend; registration cluster <*> the carrier of (TOP-REAL 2) -> special ; coherence <*> the carrier of (TOP-REAL 2) is special proofend; end; registration let p be Point of (TOP-REAL 2); cluster<*p*> -> special for FinSequence of (TOP-REAL 2); coherence for b1 being FinSequence of (TOP-REAL 2) st b1 = <*p*> holds b1 is special proofend; end; theorem Th38: :: SPPOL_2:38 for p, q being Point of (TOP-REAL 2) st ( p `1 = q `1 or p `2 = q `2 ) holds <*p,q*> is special proofend; Lm10: for f being FinSequence of (TOP-REAL 2) for n being Element of NAT st f is special holds f | n is special proofend; Lm11: for f being FinSequence of (TOP-REAL 2) for n being Element of NAT st f is special holds f /^ n is special proofend; registration let f be special FinSequence of (TOP-REAL 2); let n be Element of NAT ; clusterf | n -> special for FinSequence of (TOP-REAL 2); coherence for b1 being FinSequence of (TOP-REAL 2) st b1 = f | n holds b1 is special by Lm10; clusterf /^ n -> special for FinSequence of (TOP-REAL 2); coherence for b1 being FinSequence of (TOP-REAL 2) st b1 = f /^ n holds b1 is special by Lm11; end; theorem Th39: :: SPPOL_2:39 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st p in rng f & f is special holds f :- p is special proofend; Lm12: for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st f is special holds f -: p is special proofend; registration let f be special FinSequence of (TOP-REAL 2); let p be Point of (TOP-REAL 2); clusterf -: p -> special ; coherence f -: p is special by Lm12; end; theorem Th40: :: SPPOL_2:40 for f being FinSequence of (TOP-REAL 2) st f is special holds Rev f is special proofend; Lm13: for f, g being FinSequence of (TOP-REAL 2) st f is special & g is special & ( (f /. (len f)) `1 = (g /. 1) `1 or (f /. (len f)) `2 = (g /. 1) `2 ) holds f ^ g is special proofend; theorem Th41: :: SPPOL_2:41 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) for n being Element of NAT st f is special & p in LSeg (f,n) holds Ins (f,n,p) is special proofend; theorem Th42: :: SPPOL_2:42 for f being FinSequence of (TOP-REAL 2) for q being Point of (TOP-REAL 2) st q in rng f & 1 <> q .. f & q .. f <> len f & f is unfolded & f is s.n.c. holds (L~ (f -: q)) /\ (L~ (f :- q)) = {q} proofend; theorem Th43: :: SPPOL_2:43 for p, q being Point of (TOP-REAL 2) st p <> q & ( p `1 = q `1 or p `2 = q `2 ) holds <*p,q*> is being_S-Seq proofend; definition mode S-Sequence_in_R2 is being_S-Seq FinSequence of (TOP-REAL 2); end; registration let f be S-Sequence_in_R2; cluster Rev f -> being_S-Seq for FinSequence of (TOP-REAL 2); coherence for b1 being FinSequence of (TOP-REAL 2) st b1 = Rev f holds b1 is being_S-Seq proofend; end; theorem :: SPPOL_2:44 for i being Element of NAT for f being S-Sequence_in_R2 st i in dom f holds f /. i in L~ f proofend; theorem :: SPPOL_2:45 for p, q being Point of (TOP-REAL 2) st p <> q & ( p `1 = q `1 or p `2 = q `2 ) holds LSeg (p,q) is being_S-P_arc proofend; Lm14: for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st p in rng f holds L~ (f -: p) c= L~ f proofend; Lm15: for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st p in rng f holds L~ (f :- p) c= L~ f proofend; theorem Th46: :: SPPOL_2:46 for p being Point of (TOP-REAL 2) for f being S-Sequence_in_R2 st p in rng f & p .. f <> 1 holds f -: p is being_S-Seq proofend; theorem :: SPPOL_2:47 for p being Point of (TOP-REAL 2) for f being S-Sequence_in_R2 st p in rng f & p .. f <> len f holds f :- p is being_S-Seq proofend; theorem Th48: :: SPPOL_2:48 for p being Point of (TOP-REAL 2) for i being Element of NAT for f being S-Sequence_in_R2 st p in LSeg (f,i) & not p in rng f holds Ins (f,i,p) is being_S-Seq proofend; begin registration cluster being_S-P_arc for Element of bool the carrier of (TOP-REAL 2); existence ex b1 being Subset of (TOP-REAL 2) st b1 is being_S-P_arc proofend; end; theorem :: SPPOL_2:49 for P being Subset of (TOP-REAL 2) for p1, p2 being Point of (TOP-REAL 2) st P is_S-P_arc_joining p1,p2 holds P is_S-P_arc_joining p2,p1 proofend; definition let p1, p2 be Point of (TOP-REAL 2); let P be Subset of (TOP-REAL 2); predp1,p2 split P means :Def1: :: SPPOL_2:def 1 ( p1 <> p2 & ex f1, f2 being S-Sequence_in_R2 st ( p1 = f1 /. 1 & p1 = f2 /. 1 & p2 = f1 /. (len f1) & p2 = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,p2} & P = (L~ f1) \/ (L~ f2) ) ); end; :: deftheorem Def1 defines split SPPOL_2:def_1_:_ for p1, p2 being Point of (TOP-REAL 2) for P being Subset of (TOP-REAL 2) holds ( p1,p2 split P iff ( p1 <> p2 & ex f1, f2 being S-Sequence_in_R2 st ( p1 = f1 /. 1 & p1 = f2 /. 1 & p2 = f1 /. (len f1) & p2 = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,p2} & P = (L~ f1) \/ (L~ f2) ) ) ); theorem Th50: :: SPPOL_2:50 for P being Subset of (TOP-REAL 2) for p1, p2 being Point of (TOP-REAL 2) st p1,p2 split P holds p2,p1 split P proofend; Lm16: for P being Subset of (TOP-REAL 2) for p1, p2, q being Point of (TOP-REAL 2) for f1, f2 being S-Sequence_in_R2 st p1 = f1 /. 1 & p1 = f2 /. 1 & p2 = f1 /. (len f1) & p2 = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,p2} & P = (L~ f1) \/ (L~ f2) & q <> p1 & q in rng f1 holds ex g1, g2 being S-Sequence_in_R2 st ( p1 = g1 /. 1 & p1 = g2 /. 1 & q = g1 /. (len g1) & q = g2 /. (len g2) & (L~ g1) /\ (L~ g2) = {p1,q} & P = (L~ g1) \/ (L~ g2) ) proofend; theorem Th51: :: SPPOL_2:51 for P being Subset of (TOP-REAL 2) for p1, p2, q being Point of (TOP-REAL 2) st p1,p2 split P & q in P & q <> p1 holds p1,q split P proofend; theorem Th52: :: SPPOL_2:52 for P being Subset of (TOP-REAL 2) for p1, p2, q being Point of (TOP-REAL 2) st p1,p2 split P & q in P & q <> p2 holds q,p2 split P proofend; theorem Th53: :: SPPOL_2:53 for P being Subset of (TOP-REAL 2) for p1, p2, q1, q2 being Point of (TOP-REAL 2) st p1,p2 split P & q1 in P & q2 in P & q1 <> q2 holds q1,q2 split P proofend; notation let P be Subset of (TOP-REAL 2); synonym special_polygonal P for being_special_polygon ; end; definition let P be Subset of (TOP-REAL 2); redefine attr P is being_special_polygon means :Def2: :: SPPOL_2:def 2 ex p1, p2 being Point of (TOP-REAL 2) st p1,p2 split P; compatibility ( P is special_polygonal iff ex p1, p2 being Point of (TOP-REAL 2) st p1,p2 split P ) proofend; end; :: deftheorem Def2 defines special_polygonal SPPOL_2:def_2_:_ for P being Subset of (TOP-REAL 2) holds ( P is special_polygonal iff ex p1, p2 being Point of (TOP-REAL 2) st p1,p2 split P ); Lm17: for P being Subset of (TOP-REAL 2) st P is being_special_polygon holds ex p1, p2 being Point of (TOP-REAL 2) st ( p1 <> p2 & p1 in P & p2 in P ) proofend; definition let r1, r2, r19, r29 be real number ; func[.r1,r2,r19,r29.] -> Subset of (TOP-REAL 2) equals :: SPPOL_2:def 3 ((LSeg (|[r1,r19]|,|[r1,r29]|)) \/ (LSeg (|[r1,r29]|,|[r2,r29]|))) \/ ((LSeg (|[r2,r29]|,|[r2,r19]|)) \/ (LSeg (|[r2,r19]|,|[r1,r19]|))); coherence ((LSeg (|[r1,r19]|,|[r1,r29]|)) \/ (LSeg (|[r1,r29]|,|[r2,r29]|))) \/ ((LSeg (|[r2,r29]|,|[r2,r19]|)) \/ (LSeg (|[r2,r19]|,|[r1,r19]|))) is Subset of (TOP-REAL 2) ; end; :: deftheorem defines [. SPPOL_2:def_3_:_ for r1, r2, r19, r29 being real number holds [.r1,r2,r19,r29.] = ((LSeg (|[r1,r19]|,|[r1,r29]|)) \/ (LSeg (|[r1,r29]|,|[r2,r29]|))) \/ ((LSeg (|[r2,r29]|,|[r2,r19]|)) \/ (LSeg (|[r2,r19]|,|[r1,r19]|))); registration let n be Element of NAT ; let p1, p2 be Point of (TOP-REAL n); cluster LSeg (p1,p2) -> compact ; coherence LSeg (p1,p2) is compact ; end; registration let r1, r2, r19, r29 be real number ; cluster[.r1,r2,r19,r29.] -> non empty compact ; coherence ( not [.r1,r2,r19,r29.] is empty & [.r1,r2,r19,r29.] is compact ) proofend; end; theorem :: SPPOL_2:54 for r1, r2, r19, r29 being real number st r1 <= r2 & r19 <= r29 holds [.r1,r2,r19,r29.] = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = r1 & p `2 <= r29 & p `2 >= r19 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r29 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r19 ) or ( p `1 = r2 & p `2 <= r29 & p `2 >= r19 ) ) } proofend; theorem Th55: :: SPPOL_2:55 for r1, r2, r19, r29 being real number st r1 <> r2 & r19 <> r29 holds [.r1,r2,r19,r29.] is special_polygonal proofend; theorem Th56: :: SPPOL_2:56 R^2-unit_square = [.0,1,0,1.] ; registration cluster special_polygonal for Element of bool the carrier of (TOP-REAL 2); existence ex b1 being Subset of (TOP-REAL 2) st b1 is special_polygonal proofend; end; registration cluster R^2-unit_square -> special_polygonal ; coherence R^2-unit_square is special_polygonal by Th55, Th56; end; registration cluster special_polygonal for Element of bool the carrier of (TOP-REAL 2); existence ex b1 being Subset of (TOP-REAL 2) st b1 is special_polygonal by Th56; cluster special_polygonal -> non empty for Element of bool the carrier of (TOP-REAL 2); coherence for b1 being Subset of (TOP-REAL 2) st b1 is special_polygonal holds not b1 is empty proofend; cluster special_polygonal -> non trivial for Element of bool the carrier of (TOP-REAL 2); coherence for b1 being Subset of (TOP-REAL 2) st b1 is special_polygonal holds not b1 is trivial proofend; end; definition mode Special_polygon_in_R2 is special_polygonal Subset of (TOP-REAL 2); end; theorem Th57: :: SPPOL_2:57 for P being Subset of (TOP-REAL 2) st P is being_S-P_arc holds P is compact proofend; registration cluster special_polygonal -> compact for Element of bool the carrier of (TOP-REAL 2); coherence for b1 being Special_polygon_in_R2 holds b1 is compact proofend; end; theorem Th58: :: SPPOL_2:58 for P being Subset of (TOP-REAL 2) st P is special_polygonal holds for p1, p2 being Point of (TOP-REAL 2) st p1 <> p2 & p1 in P & p2 in P holds p1,p2 split P proofend; theorem :: SPPOL_2:59 for P being Subset of (TOP-REAL 2) st P is special_polygonal holds for p1, p2 being Point of (TOP-REAL 2) st p1 <> p2 & p1 in P & p2 in P holds ex P1, P2 being Subset of (TOP-REAL 2) st ( P1 is_S-P_arc_joining p1,p2 & P2 is_S-P_arc_joining p1,p2 & P1 /\ P2 = {p1,p2} & P = P1 \/ P2 ) proofend;