begin
theorem Th1:
for
A,
x,
y being
set st
A c= {x,y} &
x in A & not
y in A holds
A = {x}
begin
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem
theorem Th10:
theorem Th11:
theorem Th12:
Lm1:
for p being FinSequence
for m, n being Element of NAT st 1 <= m & m <= n + 1 & n <= len p holds
( (len ((m,n) -cut p)) + m = n + 1 & ( for i being Element of NAT st i < len ((m,n) -cut p) holds
((m,n) -cut p) . (i + 1) = p . (m + i) ) )
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
begin
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
Lm2:
for f being one-to-one non empty unfolded s.n.c. FinSequence of (TOP-REAL 2)
for g being one-to-one non trivial unfolded s.n.c. FinSequence of (TOP-REAL 2)
for i, j being Element of NAT st i < len f & 1 < i holds
for x being Point of (TOP-REAL 2) st x in (LSeg ((f ^' g),i)) /\ (LSeg ((f ^' g),j)) holds
x <> f /. 1
Lm3:
for f being one-to-one non empty unfolded s.n.c. FinSequence of (TOP-REAL 2)
for g being one-to-one non trivial unfolded s.n.c. FinSequence of (TOP-REAL 2)
for i, j being Element of NAT st j > len f & j + 1 < len (f ^' g) holds
for x being Point of (TOP-REAL 2) st x in (LSeg ((f ^' g),i)) /\ (LSeg ((f ^' g),j)) holds
x <> g /. (len g)
theorem Th33:
theorem Th34:
theorem Th35:
theorem