begin
theorem
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem
theorem
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
Lm1:
for f being FinSequence of (TOP-REAL 2)
for n being Element of NAT holds L~ (f | n) c= L~ f
theorem
canceled;
theorem Th25:
theorem Th26:
begin
theorem Th27:
Lm2:
for p, q being Point of (TOP-REAL 2) holds <*p,q*> is unfolded
Lm3:
for f being FinSequence of (TOP-REAL 2)
for n being Element of NAT st f is unfolded holds
f | n is unfolded
Lm4:
for f being FinSequence of (TOP-REAL 2)
for n being Element of NAT st f is unfolded holds
f /^ n is unfolded
theorem Th28:
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
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
Lm6:
for p, q being Point of (TOP-REAL 2) holds <*p,q*> is s.n.c.
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.
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.
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.
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem
canceled;
theorem Th40:
Lm10:
for f being FinSequence of (TOP-REAL 2)
for n being Element of NAT st f is special holds
f | n is special
Lm11:
for f being FinSequence of (TOP-REAL 2)
for n being Element of NAT st f is special holds
f /^ n is special
theorem Th41:
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
theorem Th42:
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
theorem
canceled;
theorem Th44:
theorem Th45:
theorem Th46:
theorem
canceled;
theorem
theorem
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
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
theorem Th50:
theorem
theorem Th52:
begin
theorem
:: 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 Th54:
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) )
theorem Th55:
theorem Th56:
theorem Th57:
:: 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 special_polygonal holds
ex p1, p2 being Point of (TOP-REAL 2) st
( p1 <> p2 & p1 in P & p2 in P )
definition
let r1,
r2,
r19,
r29 be
real number ;
func [.r1,r2,r19,r29.] -> Subset of
(TOP-REAL 2) equals
((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 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 )
end;
theorem
theorem Th59:
theorem Th60:
theorem
canceled;
theorem Th62:
theorem
canceled;
theorem Th64:
theorem