:: SPPOL_2 semantic presentation

theorem Th1: :: SPPOL_2:1

for b₁, b₂, b₃, b₄ being real number st |[b₁,b₂]| = |[b₃,b₄]| holds
( b₁ = b₃ & b₂ = b₄ )

proof end;

theorem Th2: :: SPPOL_2:2

for b₁ being FinSequence of (TOP-REAL 2)
for b₂, b₃ being Nat st b₂ + b₃ = len b₁ holds
LSeg b₁,b₂ = LSeg (Rev b₁),b₃

proof end;

theorem Th3: :: SPPOL_2:3

for b₁ being FinSequence of (TOP-REAL 2)
for b₂, b₃ being Nat st b₂ + 1 <= len (b₁ | b₃) holds
LSeg (b₁ | b₃),b₂ = LSeg b₁,b₂

proof end;

theorem Th4: :: SPPOL_2:4

for b₁ being FinSequence of (TOP-REAL 2)
for b₂, b₃ being Nat st b₂ <= len b₁ & 1 <= b₃ holds
LSeg (b₁ /^ b₂),b₃ = LSeg b₁,(b₂ + b₃)

proof end;

theorem Th5: :: SPPOL_2:5

for b₁ being FinSequence of (TOP-REAL 2)
for b₂, b₃ being Nat st 1 <= b₂ & b₂ + 1 <= (len b₁) - b₃ holds
LSeg (b₁ /^ b₃),b₂ = LSeg b₁,(b₃ + b₂)

proof end;

theorem Th6: :: SPPOL_2:6

for b₁, b₂ being FinSequence of (TOP-REAL 2)
for b₃ being Nat st b₃ + 1 <= len b₁ holds
LSeg (b₁ ^ b₂),b₃ = LSeg b₁,b₃

proof end;

theorem Th7: :: SPPOL_2:7

for b₁, b₂ being FinSequence of (TOP-REAL 2)
for b₃ being Nat st 1 <= b₃ holds
LSeg (b₁ ^ b₂),((len b₁) + b₃) = LSeg b₂,b₃

proof end;

theorem Th8: :: SPPOL_2:8

for b₁, b₂ being FinSequence of (TOP-REAL 2) st not b₁ is empty & not b₂ is empty holds
LSeg (b₁ ^ b₂),(len b₁) = LSeg (b₁ /. (len b₁)),(b₂ /. 1)

proof end;

theorem Th9: :: SPPOL_2:9

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2)
for b₃ being Nat st b₃ + 1 <= len (b₁ -: b₂) holds
LSeg (b₁ -: b₂),b₃ = LSeg b₁,b₃

proof end;

theorem Th10: :: SPPOL_2:10

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2)
for b₃ being Nat st b₂ in rng b₁ holds
LSeg (b₁ :- b₂),(b₃ + 1) = LSeg b₁,(b₃ + (b₂ .. b₁))

proof end;

theorem Th11: :: SPPOL_2:11

L~ (<*> the carrier of (TOP-REAL 2)) = {}

proof end;

theorem Th12: :: SPPOL_2:12

for b₁ being Point of (TOP-REAL 2) holds L~ <*b₁*> = {}

proof end;

theorem Th13: :: SPPOL_2:13

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st b₂ in L~ b₁ holds
ex b₃ being Nat st
( 1 <= b₃ & b₃ + 1 <= len b₁ & b₂ in LSeg b₁,b₃ )

proof end;

theorem Th14: :: SPPOL_2:14

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st b₂ in L~ b₁ holds
ex b₃ being Nat st
( 1 <= b₃ & b₃ + 1 <= len b₁ & b₂ in LSeg (b₁ /. b₃),(b₁ /. (b₃ + 1)) )

proof end;

theorem Th15: :: SPPOL_2:15

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2)
for b₃ being Nat st 1 <= b₃ & b₃ + 1 <= len b₁ & b₂ in LSeg (b₁ /. b₃),(b₁ /. (b₃ + 1)) holds
b₂ in L~ b₁

proof end;

theorem Th16: :: SPPOL_2:16

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Nat st 1 <= b₂ & b₂ + 1 <= len b₁ holds
LSeg (b₁ /. b₂),(b₁ /. (b₂ + 1)) c= L~ b₁

proof end;

theorem Th17: :: SPPOL_2:17

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2)
for b₃ being Nat st b₂ in LSeg b₁,b₃ holds
b₂ in L~ b₁

proof end;

theorem Th18: :: SPPOL_2:18

for b₁ being FinSequence of (TOP-REAL 2) st len b₁ >= 2 holds
rng b₁ c= L~ b₁

proof end;

theorem Th19: :: SPPOL_2:19

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st not b₁ is empty holds
L~ (b₁ ^ <*b₂*>) = (L~ b₁) \/ (LSeg (b₁ /. (len b₁)),b₂)

proof end;

theorem Th20: :: SPPOL_2:20

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st not b₁ is empty holds
L~ (<*b₂*> ^ b₁) = (LSeg b₂,(b₁ /. 1)) \/ (L~ b₁)

proof end;

theorem Th21: :: SPPOL_2:21

for b₁, b₂ being Point of (TOP-REAL 2) holds L~ <*b₁,b₂*> = LSeg b₁,b₂

proof end;

theorem Th22: :: SPPOL_2:22

for b₁ being FinSequence of (TOP-REAL 2) holds L~ b₁ = L~ (Rev b₁)

proof end;

theorem Th23: :: SPPOL_2:23

for b₁, b₂ being FinSequence of (TOP-REAL 2) st not b₁ is empty & not b₂ is empty holds
L~ (b₁ ^ b₂) = ((L~ b₁) \/ (LSeg (b₁ /. (len b₁)),(b₂ /. 1))) \/ (L~ b₂)

proof end;

Lemma22: for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Nat holds L~ (b₁ | b₂) c= L~ b₁

proof end;

theorem Th24: :: SPPOL_2:24

canceled;

theorem Th25: :: SPPOL_2:25

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st b₂ in rng b₁ holds
L~ b₁ = (L~ (b₁ -: b₂)) \/ (L~ (b₁ :- b₂))

proof end;

theorem Th26: :: SPPOL_2:26

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2)
for b₃ being Nat st b₂ in LSeg b₁,b₃ holds
L~ b₁ = L~ (Ins b₁,b₃,b₂)

proof end;

registration

cluster being_S-Seq FinSequence of the carrier of (TOP-REAL 2);
existence

proof end;

cluster being_S-Seq -> one-to-one non trivial special unfolded s.n.c. FinSequence of the carrier of (TOP-REAL 2);
coherence

proof end;

cluster one-to-one non trivial special unfolded s.n.c. -> being_S-Seq FinSequence of the carrier of (TOP-REAL 2);
coherence

proof end;

cluster being_S-Seq -> non empty FinSequence of the carrier of (TOP-REAL 2);
coherence

proof end;

end;

registration

cluster non empty one-to-one non trivial special unfolded s.n.c. being_S-Seq FinSequence of the carrier of (TOP-REAL 2);
existence

proof end;

end;

theorem Th27: :: SPPOL_2:27

for b₁ being FinSequence of (TOP-REAL 2) st len b₁ <= 2 holds
b₁ is unfolded

proof end;

Lemma26: for b₁, b₂ being Point of (TOP-REAL 2) holds <*b₁,b₂*> is unfolded

proof end;

Lemma27: for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Nat st b₁ is unfolded holds
b₁ | b₂ is unfolded

proof end;

Lemma28: for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Nat st b₁ is unfolded holds
b₁ /^ b₂ is unfolded

proof end;

registration

let c₁ be unfolded FinSequence of (TOP-REAL 2);
let c₂ be Nat;
cluster a₁ | a₂ -> unfolded ;
coherence by Lemma27;
cluster a₁ /^ a₂ -> unfolded ;
coherence by Lemma28;

end;

theorem Th28: :: SPPOL_2:28

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st b₂ in rng b₁ & b₁ is unfolded holds
b₁ :- b₂ is unfolded

proof end;

Lemma30: for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st b₁ is unfolded holds
b₁ -: b₂ is unfolded

proof end;

registration

let c₁ be unfolded FinSequence of (TOP-REAL 2);
let c₂ be Point of (TOP-REAL 2);
cluster a₁ -: a₂ -> unfolded ;
coherence by Lemma30;

end;

theorem Th29: :: SPPOL_2:29

for b₁ being FinSequence of (TOP-REAL 2) st b₁ is unfolded holds
Rev b₁ is unfolded

proof end;

theorem Th30: :: SPPOL_2:30

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st b₁ is unfolded & (LSeg b₂,(b₁ /. 1)) /\ (LSeg b₁,1) = {(b₁ /. 1)} holds
<*b₂*> ^ b₁ is unfolded

proof end;

theorem Th31: :: SPPOL_2:31

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2)
for b₃ being Nat st b₁ is unfolded & b₃ + 1 = len b₁ & (LSeg b₁,b₃) /\ (LSeg (b₁ /. (len b₁)),b₂) = {(b₁ /. (len b₁))} holds
b₁ ^ <*b₂*> is unfolded

proof end;

theorem Th32: :: SPPOL_2:32

for b₁, b₂ being FinSequence of (TOP-REAL 2)
for b₃ being Nat st b₁ is unfolded & b₂ is unfolded & b₃ + 1 = len b₁ & (LSeg b₁,b₃) /\ (LSeg (b₁ /. (len b₁)),(b₂ /. 1)) = {(b₁ /. (len b₁))} & (LSeg (b₁ /. (len b₁)),(b₂ /. 1)) /\ (LSeg b₂,1) = {(b₂ /. 1)} holds
b₁ ^ b₂ is unfolded

proof end;

theorem Th33: :: SPPOL_2:33

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2)
for b₃ being Nat st b₁ is unfolded & b₂ in LSeg b₁,b₃ holds
Ins b₁,b₃,b₂ is unfolded

proof end;

theorem Th34: :: SPPOL_2:34

for b₁ being FinSequence of (TOP-REAL 2) st len b₁ <= 2 holds
b₁ is s.n.c.

proof end;

Lemma37: for b₁, b₂ being Point of (TOP-REAL 2) holds <*b₁,b₂*> is s.n.c.

proof end;

Lemma38: for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Nat st b₁ is s.n.c. holds
b₁ | b₂ is s.n.c.

proof end;

Lemma39: for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Nat st b₁ is s.n.c. holds
b₁ /^ b₂ is s.n.c.

proof end;

registration

let c₁ be s.n.c. FinSequence of (TOP-REAL 2);
let c₂ be Nat;
cluster a₁ | a₂ -> s.n.c. ;
coherence by Lemma38;
cluster a₁ /^ a₂ -> s.n.c. ;
coherence by Lemma39;

end;

Lemma40: for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st b₁ is s.n.c. holds
b₁ -: b₂ is s.n.c.

proof end;

registration

let c₁ be s.n.c. FinSequence of (TOP-REAL 2);
let c₂ be Point of (TOP-REAL 2);
cluster a₁ -: a₂ -> s.n.c. ;
coherence by Lemma40;

end;

theorem Th35: :: SPPOL_2:35

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st b₂ in rng b₁ & b₁ is s.n.c. holds
b₁ :- b₂ is s.n.c.

proof end;

theorem Th36: :: SPPOL_2:36

for b₁ being FinSequence of (TOP-REAL 2) st b₁ is s.n.c. holds
Rev b₁ is s.n.c.

proof end;

theorem Th37: :: SPPOL_2:37

for b₁, b₂ being FinSequence of (TOP-REAL 2) st b₁ is s.n.c. & b₂ is s.n.c. & L~ b₁ misses L~ b₂ & ( for b₃ being Nat st 1 <= b₃ & b₃ + 2 <= len b₁ holds
LSeg b₁,b₃ misses LSeg (b₁ /. (len b₁)),(b₂ /. 1) ) & ( for b₃ being Nat st 2 <= b₃ & b₃ + 1 <= len b₂ holds
LSeg b₂,b₃ misses LSeg (b₁ /. (len b₁)),(b₂ /. 1) ) holds
b₁ ^ b₂ is s.n.c.

proof end;

theorem Th38: :: SPPOL_2:38

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2)
for b₃ being Nat st b₁ is unfolded & b₁ is s.n.c. & b₂ in LSeg b₁,b₃ & not b₂ in rng b₁ holds
Ins b₁,b₃,b₂ is s.n.c.

proof end;

Lemma45: <*> the carrier of (TOP-REAL 2) is special

proof end;

registration

cluster <*> the carrier of (TOP-REAL 2) -> special ;
coherence by Lemma45;

end;

theorem Th39: :: SPPOL_2:39

for b₁ being Point of (TOP-REAL 2) holds <*b₁*> is special

proof end;

theorem Th40: :: SPPOL_2:40

for b₁, b₂ being Point of (TOP-REAL 2) st ( b₁ `1 = b₂ `1 or b₁ `2 = b₂ `2 ) holds
<*b₁,b₂*> is special

proof end;

Lemma48: for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Nat st b₁ is special holds
b₁ | b₂ is special

proof end;

Lemma49: for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Nat st b₁ is special holds
b₁ /^ b₂ is special

proof end;

registration

let c₁ be special FinSequence of (TOP-REAL 2);
let c₂ be Nat;
cluster a₁ | a₂ -> special ;
coherence by Lemma48;
cluster a₁ /^ a₂ -> special ;
coherence by Lemma49;

end;

theorem Th41: :: SPPOL_2:41

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st b₂ in rng b₁ & b₁ is special holds
b₁ :- b₂ is special

proof end;

Lemma51: for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st b₁ is special holds
b₁ -: b₂ is special

proof end;

registration

let c₁ be special FinSequence of (TOP-REAL 2);
let c₂ be Point of (TOP-REAL 2);
cluster a₁ -: a₂ -> special ;
coherence by Lemma51;

end;

theorem Th42: :: SPPOL_2:42

for b₁ being FinSequence of (TOP-REAL 2) st b₁ is special holds
Rev b₁ is special

proof end;

Lemma53: for b₁, b₂ being FinSequence of (TOP-REAL 2) st b₁ is special & b₂ is special & ( (b₁ /. (len b₁)) `1 = (b₂ /. 1) `1 or (b₁ /. (len b₁)) `2 = (b₂ /. 1) `2 ) holds
b₁ ^ b₂ is special

proof end;

theorem Th43: :: SPPOL_2:43

canceled;

theorem Th44: :: SPPOL_2:44

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2)
for b₃ being Nat st b₁ is special & b₂ in LSeg b₁,b₃ holds
Ins b₁,b₃,b₂ is special

proof end;

theorem Th45: :: SPPOL_2:45

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st b₂ in rng b₁ & 1 <> b₂ .. b₁ & b₂ .. b₁ <> len b₁ & b₁ is unfolded & b₁ is s.n.c. holds
(L~ (b₁ -: b₂)) /\ (L~ (b₁ :- b₂)) = {b₂}

proof end;

theorem Th46: :: SPPOL_2:46

for b₁, b₂ being Point of (TOP-REAL 2) st b₁ <> b₂ & ( b₁ `1 = b₂ `1 or b₁ `2 = b₂ `2 ) holds
<*b₁,b₂*> is being_S-Seq

proof end;

definition

mode S-Sequence_in_R2 is being_S-Seq FinSequence of (TOP-REAL 2);

end;

theorem Th47: :: SPPOL_2:47

for b₁ being S-Sequence_in_R2 holds Rev b₁ is being_S-Seq

proof end;

theorem Th48: :: SPPOL_2:48

for b₁ being Nat
for b₂ being S-Sequence_in_R2 st b₁ in dom b₂ holds
b₂ /. b₁ in L~ b₂

proof end;

theorem Th49: :: SPPOL_2:49

for b₁, b₂ being Point of (TOP-REAL 2) st b₁ <> b₂ & ( b₁ `1 = b₂ `1 or b₁ `2 = b₂ `2 ) holds
LSeg b₁,b₂ is being_S-P_arc

proof end;

Lemma58: for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st b₂ in rng b₁ holds
L~ (b₁ -: b₂) c= L~ b₁

proof end;

Lemma59: for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st b₂ in rng b₁ holds
L~ (b₁ :- b₂) c= L~ b₁

proof end;

theorem Th50: :: SPPOL_2:50

for b₁ being Point of (TOP-REAL 2)
for b₂ being S-Sequence_in_R2 st b₁ in rng b₂ & b₁ .. b₂ <> 1 holds
b₂ -: b₁ is being_S-Seq

proof end;

theorem Th51: :: SPPOL_2:51

for b₁ being Point of (TOP-REAL 2)
for b₂ being S-Sequence_in_R2 st b₁ in rng b₂ & b₁ .. b₂ <> len b₂ holds
b₂ :- b₁ is being_S-Seq

proof end;

theorem Th52: :: SPPOL_2:52

for b₁ being Point of (TOP-REAL 2)
for b₂ being Nat
for b₃ being S-Sequence_in_R2 st b₁ in LSeg b₃,b₂ & not b₁ in rng b₃ holds
Ins b₃,b₂,b₁ is being_S-Seq

proof end;

registration

cluster being_S-P_arc Element of K40(the carrier of (TOP-REAL 2));
existence

proof end;

end;

theorem Th53: :: SPPOL_2:53

for b₁ being Subset of (TOP-REAL 2)
for b₂, b₃ being Point of (TOP-REAL 2) st b₁ is_S-P_arc_joining b₂,b₃ holds
b₁ is_S-P_arc_joining b₃,b₂

proof end;

definition

let c₁, c₂ be Point of (TOP-REAL 2);
let c₃ be Subset of (TOP-REAL 2);
pred c₁,c₂ split c₃ means :Def1: :: SPPOL_2:def 1
( a₁ <> a₂ & ex b₁, b₂ being S-Sequence_in_R2 st
( a₁ = b₁ /. 1 & a₁ = b₂ /. 1 & a₂ = b₁ /. (len b₁) & a₂ = b₂ /. (len b₂) & (L~ b₁) /\ (L~ b₂) = {a₁,a₂} & a₃ = (L~ b₁) \/ (L~ b₂) ) );

end;

:: deftheorem Def1 defines split SPPOL_2:def 1 :

theorem Th54: :: SPPOL_2:54

for b₁ being Subset of (TOP-REAL 2)
for b₂, b₃ being Point of (TOP-REAL 2) st b₂,b₃ split b₁ holds
b₃,b₂ split b₁

proof end;

Lemma64: for b₁ being Subset of (TOP-REAL 2)
for b₂, b₃, b₄ being Point of (TOP-REAL 2)
for b₅, b₆ being S-Sequence_in_R2 st b₂ = b₅ /. 1 & b₂ = b₆ /. 1 & b₃ = b₅ /. (len b₅) & b₃ = b₆ /. (len b₆) & (L~ b₅) /\ (L~ b₆) = {b₂,b₃} & b₁ = (L~ b₅) \/ (L~ b₆) & b₄ <> b₂ & b₄ in rng b₅ holds
ex b₇, b₈ being S-Sequence_in_R2 st
( b₂ = b₇ /. 1 & b₂ = b₈ /. 1 & b₄ = b₇ /. (len b₇) & b₄ = b₈ /. (len b₈) & (L~ b₇) /\ (L~ b₈) = {b₂,b₄} & b₁ = (L~ b₇) \/ (L~ b₈) )

proof end;

theorem Th55: :: SPPOL_2:55

for b₁ being Subset of (TOP-REAL 2)
for b₂, b₃, b₄ being Point of (TOP-REAL 2) st b₂,b₃ split b₁ & b₄ in b₁ & b₄ <> b₂ holds
b₂,b₄ split b₁

proof end;

theorem Th56: :: SPPOL_2:56

for b₁ being Subset of (TOP-REAL 2)
for b₂, b₃, b₄ being Point of (TOP-REAL 2) st b₂,b₃ split b₁ & b₄ in b₁ & b₄ <> b₃ holds
b₄,b₃ split b₁

proof end;

theorem Th57: :: SPPOL_2:57

for b₁ being Subset of (TOP-REAL 2)
for b₂, b₃, b₄, b₅ being Point of (TOP-REAL 2) st b₂,b₃ split b₁ & b₄ in b₁ & b₅ in b₁ & b₄ <> b₅ holds
b₄,b₅ split b₁

proof end;

notation

let c₁ be Subset of (TOP-REAL 2);
synonym special_polygonal c₁ for being_special_polygon c₁;

end;

definition

let c₁ be Subset of (TOP-REAL 2);
redefine attr a₁ is being_special_polygon means :Def2: :: SPPOL_2:def 2
ex b₁, b₂ being Point of (TOP-REAL 2) st b₁,b₂ split a₁;
compatibility

proof end;

end;

:: deftheorem Def2 defines special_polygonal SPPOL_2:def 2 :

Lemma69: for b₁ being Subset of (TOP-REAL 2) st b₁ is special_polygonal holds
ex b₂, b₃ being Point of (TOP-REAL 2) st
( b₂ <> b₃ & b₂ in b₁ & b₃ in b₁ )

proof end;

definition

let c₁, c₂, c₃, c₄ be real number ;
func [.c₁,c₂,c₃,c₄.] -> Subset of (TOP-REAL 2) equals :: SPPOL_2:def 3
((LSeg |[a₁,a₃]|,|[a₁,a₄]|) \/ (LSeg |[a₁,a₄]|,|[a₂,a₄]|)) \/ ((LSeg |[a₂,a₄]|,|[a₂,a₃]|) \/ (LSeg |[a₂,a₃]|,|[a₁,a₃]|));
coherence ;

end;

:: deftheorem Def3 defines [. SPPOL_2:def 3 :

registration

let c₁ be Nat;
let c₂, c₃ be Point of (TOP-REAL c₁);
cluster LSeg a₂,a₃ -> compact ;
coherence by SPPOL_1:28;

end;

registration

let c₁, c₂, c₃, c₄ be real number ;
cluster [.a₁,a₂,a₃,a₄.] -> non empty compact ;
coherence

proof end;

end;

theorem Th58: :: SPPOL_2:58

for b₁, b₂, b₃, b₄ being real number st b₁ <= b₂ & b₃ <= b₄ holds
[.b₁,b₂,b₃,b₄.] = { b₅ where B is Point of (TOP-REAL 2) : ( ( b₅ `1 = b₁ & b₅ `2 <= b₄ & b₅ `2 >= b₃ ) or ( b₅ `1 <= b₂ & b₅ `1 >= b₁ & b₅ `2 = b₄ ) or ( b₅ `1 <= b₂ & b₅ `1 >= b₁ & b₅ `2 = b₃ ) or ( b₅ `1 = b₂ & b₅ `2 <= b₄ & b₅ `2 >= b₃ ) ) }

proof end;

theorem Th59: :: SPPOL_2:59

for b₁, b₂, b₃, b₄ being real number st b₁ <> b₂ & b₃ <> b₄ holds
[.b₁,b₂,b₃,b₄.] is special_polygonal

proof end;

theorem Th60: :: SPPOL_2:60

R^2-unit_square = [.0,1,0,1.] ;

registration

cluster special_polygonal Element of K40(the carrier of (TOP-REAL 2));
existence

proof end;

end;

theorem Th61: :: SPPOL_2:61

R^2-unit_square is special_polygonal by Th59, Th60;

registration

cluster special_polygonal Element of K40(the carrier of (TOP-REAL 2));
existence by Th61;
cluster special_polygonal -> non empty Element of K40(the carrier of (TOP-REAL 2));
coherence

proof end;

cluster special_polygonal -> non trivial Element of K40(the carrier of (TOP-REAL 2));
coherence

proof end;

end;

definition

mode Special_polygon_in_R2 is special_polygonal Subset of (TOP-REAL 2);

end;

theorem Th62: :: SPPOL_2:62

for b₁ being Subset of (TOP-REAL 2) st b₁ is being_S-P_arc holds
b₁ is compact

proof end;

theorem Th63: :: SPPOL_2:63

for b₁ being Special_polygon_in_R2 holds b₁ is compact

proof end;

theorem Th64: :: SPPOL_2:64

for b₁ being Subset of (TOP-REAL 2) st b₁ is special_polygonal holds
for b₂, b₃ being Point of (TOP-REAL 2) st b₂ <> b₃ & b₂ in b₁ & b₃ in b₁ holds
b₂,b₃ split b₁

proof end;

theorem Th65: :: SPPOL_2:65

for b₁ being Subset of (TOP-REAL 2) st b₁ is special_polygonal holds
for b₂, b₃ being Point of (TOP-REAL 2) st b₂ <> b₃ & b₂ in b₁ & b₃ in b₁ holds
ex b₄, b₅ being Subset of (TOP-REAL 2) st
( b₄ is_S-P_arc_joining b₂,b₃ & b₅ is_S-P_arc_joining b₂,b₃ & b₄ /\ b₅ = {b₂,b₃} & b₁ = b₄ \/ b₅ )

proof end;