begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
for
n,
k being
Nat st
n < k holds
n <= k - 1
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th15:
theorem
begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th20:
theorem
canceled;
theorem
canceled;
theorem
theorem Th24:
theorem
for
n being
Element of
NAT for
p1,
p2,
q1,
q2 being
Point of holds
( not
LSeg p1,
p2 = LSeg q1,
q2 or (
p1 = q1 &
p2 = q2 ) or (
p1 = q2 &
p2 = q1 ) )
theorem
theorem
canceled;
theorem Th28:
theorem
:: deftheorem Def1 defines is_extremal_in SPPOL_1:def 1 :
theorem
theorem
theorem Th32:
theorem
theorem
begin
theorem Th35:
:: deftheorem Def2 defines horizontal SPPOL_1:def 2 :
:: deftheorem Def3 defines vertical SPPOL_1:def 3 :
Lm1:
for P being Subset of st not P is trivial & P is horizontal holds
not P is vertical
theorem Th36:
theorem Th37:
theorem
theorem
theorem Th40:
theorem Th41:
theorem Th42:
theorem
theorem Th44:
theorem Th45:
Lm2:
for f being FinSequence of the carrier of (TOP-REAL 2)
for k being Element of NAT holds { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f & i <> k & i <> k + 1 ) } is finite
theorem
theorem Th47:
Lm3:
for f being FinSequence of the carrier of (TOP-REAL 2)
for k being Element of NAT holds { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f & i <> k & i <> k + 1 ) } is Subset-Family of
theorem Th48:
theorem
Lm4:
for f being FinSequence of the carrier of (TOP-REAL 2)
for Q being Subset of
for k being Element of NAT st Q = union { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f & i <> k & i <> k + 1 ) } holds
Q is closed
:: deftheorem Def4 defines alternating SPPOL_1:def 4 :
theorem Th50:
theorem Th51:
theorem Th52:
theorem
Lm5:
for f being FinSequence of the carrier of (TOP-REAL 2)
for i being Element of NAT
for p1, p2 being Point of st f is alternating & 1 <= i & i + 2 <= len f & p1 = f /. i & p2 = f /. (i + 2) holds
ex p being Point of st
( p in LSeg p1,p2 & p `1 <> p1 `1 & p `1 <> p2 `1 & p `2 <> p1 `2 & p `2 <> p2 `2 )
theorem
theorem Th55:
theorem Th56:
theorem
theorem Th58:
theorem Th59:
theorem Th60:
:: deftheorem Def5 defines are_generators_of SPPOL_1:def 5 :
theorem
theorem
theorem
theorem