:: SPPOL_1 semantic presentation

theorem Th1: :: SPPOL_1:1

canceled;

theorem Th2: :: SPPOL_1:2

canceled;

theorem Th3: :: SPPOL_1:3

canceled;

theorem Th4: :: SPPOL_1:4

canceled;

theorem Th5: :: SPPOL_1:5

for b₁, b₂ being real number st b₁ <= b₂ holds
( b₁ - 1 <= b₂ & b₁ - 1 < b₂ & b₁ <= b₂ + 1 & b₁ < b₂ + 1 ) by XREAL_1:147, XREAL_1:149;

theorem Th6: :: SPPOL_1:6

for b₁, b₂ being Nat st b₁ < b₂ holds
b₁ <= b₂ - 1

proof end;

theorem Th7: :: SPPOL_1:7

for b₁, b₂, b₃ being Nat st 1 <= b₁ - b₂ & b₁ - b₂ <= b₃ holds
( b₁ - b₂ in Seg b₃ & b₁ - b₂ is Nat )

proof end;

Lemma1: for b₁, b₂, b₃, b₄ being real number st b₁ >= 0 & b₂ >= 0 & b₃ >= 0 & b₄ >= 0 & (b₁ * b₃) + (b₂ * b₄) = 0 holds
( ( b₁ = 0 or b₃ = 0 ) & ( b₂ = 0 or b₄ = 0 ) )
by XREAL_1:73;

theorem Th8: :: SPPOL_1:8

canceled;

theorem Th9: :: SPPOL_1:9

canceled;

theorem Th10: :: SPPOL_1:10

canceled;

theorem Th11: :: SPPOL_1:11

canceled;

theorem Th12: :: SPPOL_1:12

for b₁, b₂, b₃ being real number st 0 <= b₁ & b₁ <= 1 & b₂ >= 0 & b₃ >= 0 & (b₁ * b₂) + ((1 - b₁) * b₃) = 0 & not ( b₁ = 0 & b₃ = 0 ) & not ( b₁ = 1 & b₂ = 0 ) holds
( b₂ = 0 & b₃ = 0 )

proof end;

theorem Th13: :: SPPOL_1:13

for b₁, b₂, b₃ being real number st b₁ < b₂ & b₁ < b₃ holds
b₁ < min b₂,b₃

proof end;

theorem Th14: :: SPPOL_1:14

for b₁, b₂, b₃ being real number st b₁ > b₂ & b₁ > b₃ holds
b₁ > max b₂,b₃

proof end;

scheme :: SPPOL_1:sch 1
s1{ F₁() -> non empty set , F₂() -> FinSequence of F₁(), F₃( FinSequence of F₁(), Nat) -> set , P₁[ Nat] } :

{ F₃(F₂(),b₁) where B is Nat : ( b₁ in dom F₂() & P₁[b₁] ) } is finite

proof end;

scheme :: SPPOL_1:sch 2
s2{ F₁() -> non empty set , F₂() -> FinSequence of F₁(), F₃( FinSequence of F₁(), Nat) -> set , P₁[ Nat] } :

{ F₃(F₂(),b₁) where B is Nat : ( 1 <= b₁ & b₁ <= len F₂() & P₁[b₁] ) } is finite

proof end;

theorem Th15: :: SPPOL_1:15

for b₁ being Nat
for b₂, b₃, b₄ being Element of REAL b₁ holds |.(b₂ - b₃).| - |.(b₃ - b₄).| <= |.(b₂ - b₄).|

proof end;

theorem Th16: :: SPPOL_1:16

for b₁ being Nat
for b₂, b₃, b₄ being Element of REAL b₁ holds |.(b₃ - b₂).| - |.(b₃ - b₄).| <= |.(b₄ - b₂).|

proof end;

theorem Th17: :: SPPOL_1:17

for b₁ being Nat
for b₂ being Point of (TOP-REAL b₁) holds
( b₂ is Element of REAL b₁ & b₂ is Point of (Euclid b₁) ) by EUCLID:25;

theorem Th18: :: SPPOL_1:18

for b₁ being Nat
for b₂ being Point of (Euclid b₁) holds
( b₂ is Element of REAL b₁ & b₂ is Point of (TOP-REAL b₁) ) by EUCLID:25;

theorem Th19: :: SPPOL_1:19

for b₁ being Nat
for b₂ being Element of REAL b₁ holds
( b₂ is Point of (Euclid b₁) & b₂ is Point of (TOP-REAL b₁) ) by EUCLID:25;

theorem Th20: :: SPPOL_1:20

for b₁ being Nat
for b₂, b₃ being Point of (Euclid b₁)
for b₄, b₅ being Element of REAL b₁ st b₄ = b₂ & b₅ = b₃ holds
dist b₂,b₃ = |.(b₄ - b₅).|

proof end;

theorem Th21: :: SPPOL_1:21

for b₁ being Nat
for b₂, b₃, b₄ being Point of (TOP-REAL b₁) st b₂ in LSeg b₃,b₄ holds
ex b₅ being Real st
( 0 <= b₅ & b₅ <= 1 & b₂ = ((1 - b₅) * b₃) + (b₅ * b₄) )

proof end;

theorem Th22: :: SPPOL_1:22

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁)
for b₄ being Real st 0 <= b₄ & b₄ <= 1 holds
((1 - b₄) * b₂) + (b₄ * b₃) in LSeg b₂,b₃ ;

theorem Th23: :: SPPOL_1:23

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁)
for b₄ being non empty Subset of (TOP-REAL b₁) st b₄ is closed & b₄ c= LSeg b₂,b₃ holds
ex b₅ being Real st
( ((1 - b₅) * b₂) + (b₅ * b₃) in b₄ & ( for b₆ being Real st 0 <= b₆ & b₆ <= 1 & ((1 - b₆) * b₂) + (b₆ * b₃) in b₄ holds
b₅ <= b₆ ) )

proof end;

theorem Th24: :: SPPOL_1:24

for b₁ being Nat
for b₂, b₃, b₄, b₅ being Point of (TOP-REAL b₁) st LSeg b₄,b₅ c= LSeg b₂,b₃ & b₂ in LSeg b₄,b₅ & not b₂ = b₄ holds
b₂ = b₅

proof end;

theorem Th25: :: SPPOL_1:25

for b₁ being Nat
for b₂, b₃, b₄, b₅ being Point of (TOP-REAL b₁) holds
( not LSeg b₂,b₃ = LSeg b₄,b₅ or ( b₂ = b₄ & b₃ = b₅ ) or ( b₂ = b₅ & b₃ = b₄ ) )

proof end;

theorem Th26: :: SPPOL_1:26

for b₁ being Nat holds TOP-REAL b₁ is_T2 ;

theorem Th27: :: SPPOL_1:27

for b₁ being Nat
for b₂ being Point of (TOP-REAL b₁) holds {b₂} is closed by PCOMPS_1:10;

theorem Th28: :: SPPOL_1:28

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁) holds LSeg b₂,b₃ is compact

proof end;

theorem Th29: :: SPPOL_1:29

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁) holds LSeg b₂,b₃ is closed

proof end;

definition

let c₁ be Nat;
let c₂ be Point of (TOP-REAL c₁);
let c₃ be Subset of (TOP-REAL c₁);
pred c₂ is_extremal_in c₃ means :Def1: :: SPPOL_1:def 1
( a₂ in a₃ & ( for b₁, b₂ being Point of (TOP-REAL a₁) st a₂ in LSeg b₁,b₂ & LSeg b₁,b₂ c= a₃ & not a₂ = b₁ holds
a₂ = b₂ ) );

end;

:: deftheorem Def1 defines is_extremal_in SPPOL_1:def 1 :

theorem Th30: :: SPPOL_1:30

for b₁ being Nat
for b₂ being Point of (TOP-REAL b₁)
for b₃, b₄ being Subset of (TOP-REAL b₁) st b₂ is_extremal_in b₃ & b₄ c= b₃ & b₂ in b₄ holds
b₂ is_extremal_in b₄

proof end;

theorem Th31: :: SPPOL_1:31

for b₁ being Nat
for b₂ being Point of (TOP-REAL b₁) holds b₂ is_extremal_in {b₂}

proof end;

theorem Th32: :: SPPOL_1:32

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁) holds b₂ is_extremal_in LSeg b₂,b₃

proof end;

theorem Th33: :: SPPOL_1:33

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁) holds b₂ is_extremal_in LSeg b₃,b₂ by Th32;

theorem Th34: :: SPPOL_1:34

for b₁ being Nat
for b₂, b₃, b₄ being Point of (TOP-REAL b₁) holds
( not b₂ is_extremal_in LSeg b₃,b₄ or b₂ = b₃ or b₂ = b₄ )

proof end;

theorem Th35: :: SPPOL_1:35

for b₁, b₂ being Point of (TOP-REAL 2) st b₁ `1 <> b₂ `1 & b₁ `2 <> b₂ `2 holds
ex b₃ being Point of (TOP-REAL 2) st
( b₃ in LSeg b₁,b₂ & b₃ `1 <> b₁ `1 & b₃ `1 <> b₂ `1 & b₃ `2 <> b₁ `2 & b₃ `2 <> b₂ `2 )

proof end;

definition

let c₁ be Subset of (TOP-REAL 2);
attr a₁ is horizontal means :Def2: :: SPPOL_1:def 2
for b₁, b₂ being Point of (TOP-REAL 2) st b₁ in a₁ & b₂ in a₁ holds
b₁ `2 = b₂ `2 ;
attr a₁ is vertical means :Def3: :: SPPOL_1:def 3
for b₁, b₂ being Point of (TOP-REAL 2) st b₁ in a₁ & b₂ in a₁ holds
b₁ `1 = b₂ `1 ;

end;

:: deftheorem Def2 defines horizontal SPPOL_1:def 2 :

:: deftheorem Def3 defines vertical SPPOL_1:def 3 :

Lemma17: for b₁ being Subset of (TOP-REAL 2) st not b₁ is trivial & b₁ is horizontal holds
not b₁ is vertical

proof end;

registration

cluster non trivial horizontal -> non vertical Element of K40(the carrier of (TOP-REAL 2));
coherence by Lemma17;
cluster non trivial vertical -> non horizontal Element of K40(the carrier of (TOP-REAL 2));
coherence by Lemma17;

end;

theorem Th36: :: SPPOL_1:36

for b₁, b₂ being Point of (TOP-REAL 2) holds
( b₁ `2 = b₂ `2 iff LSeg b₁,b₂ is horizontal )

proof end;

theorem Th37: :: SPPOL_1:37

for b₁, b₂ being Point of (TOP-REAL 2) holds
( b₁ `1 = b₂ `1 iff LSeg b₁,b₂ is vertical )

proof end;

theorem Th38: :: SPPOL_1:38

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2) st b₁ in LSeg b₂,b₃ & b₄ in LSeg b₂,b₃ & b₁ `1 <> b₄ `1 & b₁ `2 = b₄ `2 holds
LSeg b₂,b₃ is horizontal

proof end;

theorem Th39: :: SPPOL_1:39

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2) st b₁ in LSeg b₂,b₃ & b₄ in LSeg b₂,b₃ & b₁ `2 <> b₄ `2 & b₁ `1 = b₄ `1 holds
LSeg b₂,b₃ is vertical

proof end;

theorem Th40: :: SPPOL_1:40

for b₁ being Nat
for b₂ being FinSequence of the carrier of (TOP-REAL 2) holds LSeg b₂,b₁ is closed

proof end;

theorem Th41: :: SPPOL_1:41

for b₁ being Nat
for b₂ being FinSequence of the carrier of (TOP-REAL 2) holds
( not b₂ is special or LSeg b₂,b₁ is vertical or LSeg b₂,b₁ is horizontal )

proof end;

theorem Th42: :: SPPOL_1:42

for b₁ being Nat
for b₂ being FinSequence of the carrier of (TOP-REAL 2) st b₂ is one-to-one & 1 <= b₁ & b₁ + 1 <= len b₂ holds
not LSeg b₂,b₁ is trivial

proof end;

theorem Th43: :: SPPOL_1:43

for b₁ being Nat
for b₂ being FinSequence of the carrier of (TOP-REAL 2) st b₂ is one-to-one & 1 <= b₁ & b₁ + 1 <= len b₂ & LSeg b₂,b₁ is vertical holds
not LSeg b₂,b₁ is horizontal

proof end;

theorem Th44: :: SPPOL_1:44

for b₁ being FinSequence of the carrier of (TOP-REAL 2) holds { (LSeg b₁,b₂) where B is Nat : ( 1 <= b₂ & b₂ <= len b₁ ) } is finite

proof end;

theorem Th45: :: SPPOL_1:45

for b₁ being FinSequence of the carrier of (TOP-REAL 2) holds { (LSeg b₁,b₂) where B is Nat : ( 1 <= b₂ & b₂ + 1 <= len b₁ ) } is finite

proof end;

Lemma25: for b₁ being FinSequence of the carrier of (TOP-REAL 2)
for b₂ being Nat holds { (LSeg b₁,b₃) where B is Nat : ( 1 <= b₃ & b₃ + 1 <= len b₁ & b₃ <> b₂ & b₃ <> b₂ + 1 ) } is finite

proof end;

theorem Th46: :: SPPOL_1:46

for b₁ being FinSequence of the carrier of (TOP-REAL 2) holds { (LSeg b₁,b₂) where B is Nat : ( 1 <= b₂ & b₂ <= len b₁ ) } is Subset-Family of (TOP-REAL 2)

proof end;

theorem Th47: :: SPPOL_1:47

for b₁ being FinSequence of the carrier of (TOP-REAL 2) holds { (LSeg b₁,b₂) where B is Nat : ( 1 <= b₂ & b₂ + 1 <= len b₁ ) } is Subset-Family of (TOP-REAL 2)

proof end;

Lemma27: for b₁ being FinSequence of the carrier of (TOP-REAL 2)
for b₂ being Nat holds { (LSeg b₁,b₃) where B is Nat : ( 1 <= b₃ & b₃ + 1 <= len b₁ & b₃ <> b₂ & b₃ <> b₂ + 1 ) } is Subset-Family of (TOP-REAL 2)

proof end;

theorem Th48: :: SPPOL_1:48

for b₁ being Subset of (TOP-REAL 2)
for b₂ being FinSequence of the carrier of (TOP-REAL 2) st b₁ = union { (LSeg b₂,b₃) where B is Nat : ( 1 <= b₃ & b₃ + 1 <= len b₂ ) } holds
b₁ is closed

proof end;

theorem Th49: :: SPPOL_1:49

for b₁ being FinSequence of the carrier of (TOP-REAL 2) holds L~ b₁ is closed by Th48;

Lemma29: for b₁ being FinSequence of the carrier of (TOP-REAL 2)
for b₂ being Subset of (TOP-REAL 2)
for b₃ being Nat st b₂ = union { (LSeg b₁,b₄) where B is Nat : ( 1 <= b₄ & b₄ + 1 <= len b₁ & b₄ <> b₃ & b₄ <> b₃ + 1 ) } holds
b₂ is closed

proof end;

definition

let c₁ be FinSequence of (TOP-REAL 2);
attr a₁ is alternating means :Def4: :: SPPOL_1:def 4
for b₁ being Nat st 1 <= b₁ & b₁ + 2 <= len a₁ holds
( (a₁ /. b₁) `1 <> (a₁ /. (b₁ + 2)) `1 & (a₁ /. b₁) `2 <> (a₁ /. (b₁ + 2)) `2 );

end;

:: deftheorem Def4 defines alternating SPPOL_1:def 4 :

theorem Th50: :: SPPOL_1:50

for b₁ being Nat
for b₂ being FinSequence of the carrier of (TOP-REAL 2) st b₂ is special & b₂ is alternating & 1 <= b₁ & b₁ + 2 <= len b₂ & (b₂ /. b₁) `1 = (b₂ /. (b₁ + 1)) `1 holds
(b₂ /. (b₁ + 1)) `2 = (b₂ /. (b₁ + 2)) `2

proof end;

theorem Th51: :: SPPOL_1:51

for b₁ being Nat
for b₂ being FinSequence of the carrier of (TOP-REAL 2) st b₂ is special & b₂ is alternating & 1 <= b₁ & b₁ + 2 <= len b₂ & (b₂ /. b₁) `2 = (b₂ /. (b₁ + 1)) `2 holds
(b₂ /. (b₁ + 1)) `1 = (b₂ /. (b₁ + 2)) `1

proof end;

theorem Th52: :: SPPOL_1:52

for b₁ being Nat
for b₂ being FinSequence of the carrier of (TOP-REAL 2)
for b₃, b₄, b₅ being Point of (TOP-REAL 2) st b₂ is special & b₂ is alternating & 1 <= b₁ & b₁ + 2 <= len b₂ & b₃ = b₂ /. b₁ & b₄ = b₂ /. (b₁ + 1) & b₅ = b₂ /. (b₁ + 2) & not ( b₃ `1 = b₄ `1 & b₅ `1 <> b₄ `1 ) holds
( b₃ `2 = b₄ `2 & b₅ `2 <> b₄ `2 )

proof end;

theorem Th53: :: SPPOL_1:53

for b₁ being Nat
for b₂ being FinSequence of the carrier of (TOP-REAL 2)
for b₃, b₄, b₅ being Point of (TOP-REAL 2) st b₂ is special & b₂ is alternating & 1 <= b₁ & b₁ + 2 <= len b₂ & b₃ = b₂ /. b₁ & b₄ = b₂ /. (b₁ + 1) & b₅ = b₂ /. (b₁ + 2) & not ( b₄ `1 = b₅ `1 & b₃ `1 <> b₄ `1 ) holds
( b₄ `2 = b₅ `2 & b₃ `2 <> b₄ `2 )

proof end;

Lemma34: for b₁ being FinSequence of the carrier of (TOP-REAL 2)
for b₂ being Nat
for b₃, b₄ being Point of (TOP-REAL 2) st b₁ is alternating & 1 <= b₂ & b₂ + 2 <= len b₁ & b₃ = b₁ /. b₂ & b₄ = b₁ /. (b₂ + 2) holds
ex b₅ being Point of (TOP-REAL 2) st
( b₅ in LSeg b₃,b₄ & b₅ `1 <> b₃ `1 & b₅ `1 <> b₄ `1 & b₅ `2 <> b₃ `2 & b₅ `2 <> b₄ `2 )

proof end;

theorem Th54: :: SPPOL_1:54

for b₁ being Nat
for b₂ being FinSequence of the carrier of (TOP-REAL 2) st b₂ is special & b₂ is alternating & 1 <= b₁ & b₁ + 2 <= len b₂ holds
not LSeg (b₂ /. b₁),(b₂ /. (b₁ + 2)) c= (LSeg b₂,b₁) \/ (LSeg b₂,(b₁ + 1))

proof end;

theorem Th55: :: SPPOL_1:55

for b₁ being Nat
for b₂ being FinSequence of the carrier of (TOP-REAL 2) st b₂ is special & b₂ is alternating & 1 <= b₁ & b₁ + 2 <= len b₂ & LSeg b₂,b₁ is vertical holds
LSeg b₂,(b₁ + 1) is horizontal

proof end;

theorem Th56: :: SPPOL_1:56

for b₁ being Nat
for b₂ being FinSequence of the carrier of (TOP-REAL 2) st b₂ is special & b₂ is alternating & 1 <= b₁ & b₁ + 2 <= len b₂ & LSeg b₂,b₁ is horizontal holds
LSeg b₂,(b₁ + 1) is vertical

proof end;

theorem Th57: :: SPPOL_1:57

for b₁ being Nat
for b₂ being FinSequence of the carrier of (TOP-REAL 2) st b₂ is special & b₂ is alternating & 1 <= b₁ & b₁ + 2 <= len b₂ & not ( LSeg b₂,b₁ is vertical & LSeg b₂,(b₁ + 1) is horizontal ) holds
( LSeg b₂,b₁ is horizontal & LSeg b₂,(b₁ + 1) is vertical )

proof end;

theorem Th58: :: SPPOL_1:58

for b₁ being Nat
for b₂ being FinSequence of the carrier of (TOP-REAL 2)
for b₃, b₄ being Point of (TOP-REAL 2) st b₂ is special & b₂ is alternating & 1 <= b₁ & b₁ + 2 <= len b₂ & b₂ /. (b₁ + 1) in LSeg b₃,b₄ & LSeg b₃,b₄ c= (LSeg b₂,b₁) \/ (LSeg b₂,(b₁ + 1)) & not b₂ /. (b₁ + 1) = b₃ holds
b₂ /. (b₁ + 1) = b₄

proof end;

theorem Th59: :: SPPOL_1:59

for b₁ being Nat
for b₂ being FinSequence of the carrier of (TOP-REAL 2) st b₂ is special & b₂ is alternating & 1 <= b₁ & b₁ + 2 <= len b₂ holds
b₂ /. (b₁ + 1) is_extremal_in (LSeg b₂,b₁) \/ (LSeg b₂,(b₁ + 1))

proof end;

theorem Th60: :: SPPOL_1:60

for b₁ being Nat
for b₂ being FinSequence of the carrier of (TOP-REAL 2)
for b₃, b₄ being Point of (TOP-REAL 2)
for b₅ being Point of (Euclid 2) st b₂ is special & b₂ is alternating & 1 <= b₁ & b₁ + 2 <= len b₂ & b₅ = b₂ /. (b₁ + 1) & b₂ /. (b₁ + 1) in LSeg b₃,b₄ & b₂ /. (b₁ + 1) <> b₄ & not b₃ in (LSeg b₂,b₁) \/ (LSeg b₂,(b₁ + 1)) holds
for b₆ being Real st b₆ > 0 holds
ex b₇ being Point of (TOP-REAL 2) st
( not b₇ in (LSeg b₂,b₁) \/ (LSeg b₂,(b₁ + 1)) & b₇ in LSeg b₃,b₄ & b₇ in Ball b₅,b₆ )

proof end;

definition

let c₁, c₂ be FinSequence of the carrier of (TOP-REAL 2);
let c₃ be Subset of (TOP-REAL 2);
pred c₁,c₂ are_generators_of c₃ means :Def5: :: SPPOL_1:def 5
( a₁ is alternating & a₁ is being_S-Seq & a₂ is alternating & a₂ is being_S-Seq & a₁ /. 1 = a₂ /. 1 & a₁ /. (len a₁) = a₂ /. (len a₂) & <*(a₁ /. 2),(a₁ /. 1),(a₂ /. 2)*> is alternating & <*(a₁ /. ((len a₁) - 1)),(a₁ /. (len a₁)),(a₂ /. ((len a₂) - 1))*> is alternating & a₁ /. 1 <> a₁ /. (len a₁) & (L~ a₁) /\ (L~ a₂) = {(a₁ /. 1),(a₁ /. (len a₁))} & a₃ = (L~ a₁) \/ (L~ a₂) );

end;

:: deftheorem Def5 defines are_generators_of SPPOL_1:def 5 :

theorem Th61: :: SPPOL_1:61

for b₁ being Nat
for b₂ being Subset of (TOP-REAL 2)
for b₃, b₄ being FinSequence of the carrier of (TOP-REAL 2) st b₃,b₄ are_generators_of b₂ & 1 < b₁ & b₁ < len b₃ holds
b₃ /. b₁ is_extremal_in b₂

proof end;