:: by Czes\law Byli\'nski and Yatsuka Nakamura

::

:: Received January 30, 1995

:: Copyright (c) 1995-2019 Association of Mizar Users

theorem :: SPPOL_2:1

theorem Th2: :: SPPOL_2:2

for f being FinSequence of (TOP-REAL 2)

for i, j being Nat st i + j = len f holds

LSeg (f,i) = LSeg ((Rev f),j)

for i, j being Nat st i + j = len f holds

LSeg (f,i) = LSeg ((Rev f),j)

proof end;

theorem Th3: :: SPPOL_2:3

for f being FinSequence of (TOP-REAL 2)

for i, n being Nat st i + 1 <= len (f | n) holds

LSeg ((f | n),i) = LSeg (f,i)

for i, n being Nat st i + 1 <= len (f | n) holds

LSeg ((f | n),i) = LSeg (f,i)

proof end;

theorem Th4: :: SPPOL_2:4

for f being FinSequence of (TOP-REAL 2)

for i, n being Nat st n <= len f & 1 <= i holds

LSeg ((f /^ n),i) = LSeg (f,(n + i))

for i, n being Nat st n <= len f & 1 <= i holds

LSeg ((f /^ n),i) = LSeg (f,(n + i))

proof end;

theorem Th5: :: SPPOL_2:5

for f being FinSequence of (TOP-REAL 2)

for i, n being Nat st 1 <= i & i + 1 <= (len f) - n holds

LSeg ((f /^ n),i) = LSeg (f,(n + i))

for i, n being Nat st 1 <= i & i + 1 <= (len f) - n holds

LSeg ((f /^ n),i) = LSeg (f,(n + i))

proof end;

theorem Th6: :: SPPOL_2:6

for f, g being FinSequence of (TOP-REAL 2)

for i being Nat st i + 1 <= len f holds

LSeg ((f ^ g),i) = LSeg (f,i)

for i being Nat st i + 1 <= len f holds

LSeg ((f ^ g),i) = LSeg (f,i)

proof end;

theorem Th7: :: SPPOL_2:7

for f, g being FinSequence of (TOP-REAL 2)

for i being Nat st 1 <= i holds

LSeg ((f ^ g),((len f) + i)) = LSeg (g,i)

for i being Nat st 1 <= i holds

LSeg ((f ^ g),((len f) + i)) = LSeg (g,i)

proof end;

theorem Th8: :: SPPOL_2:8

for f, g being FinSequence of (TOP-REAL 2) st not f is empty & not g is empty holds

LSeg ((f ^ g),(len f)) = LSeg ((f /. (len f)),(g /. 1))

LSeg ((f ^ g),(len f)) = LSeg ((f /. (len f)),(g /. 1))

proof end;

theorem Th9: :: SPPOL_2:9

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2)

for i being Nat st i + 1 <= len (f -: p) holds

LSeg ((f -: p),i) = LSeg (f,i)

for p being Point of (TOP-REAL 2)

for i being Nat st i + 1 <= len (f -: p) holds

LSeg ((f -: p),i) = LSeg (f,i)

proof end;

theorem Th10: :: SPPOL_2:10

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2)

for i being Nat st p in rng f holds

LSeg ((f :- p),(i + 1)) = LSeg (f,(i + (p .. f)))

for p being Point of (TOP-REAL 2)

for i being Nat st p in rng f holds

LSeg ((f :- p),(i + 1)) = LSeg (f,(i + (p .. f)))

proof end;

theorem Th13: :: SPPOL_2:13

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st p in L~ f holds

ex i being Nat st

( 1 <= i & i + 1 <= len f & p in LSeg (f,i) )

for p being Point of (TOP-REAL 2) st p in L~ f holds

ex i being Nat st

( 1 <= i & i + 1 <= len f & p in LSeg (f,i) )

proof end;

theorem Th14: :: SPPOL_2:14

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st p in L~ f holds

ex i being Nat st

( 1 <= i & i + 1 <= len f & p in LSeg ((f /. i),(f /. (i + 1))) )

for p being Point of (TOP-REAL 2) st p in L~ f holds

ex i being Nat st

( 1 <= i & i + 1 <= len f & p in LSeg ((f /. i),(f /. (i + 1))) )

proof end;

theorem Th15: :: SPPOL_2:15

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2)

for i being Nat st 1 <= i & i + 1 <= len f & p in LSeg ((f /. i),(f /. (i + 1))) holds

p in L~ f

for p being Point of (TOP-REAL 2)

for i being Nat st 1 <= i & i + 1 <= len f & p in LSeg ((f /. i),(f /. (i + 1))) holds

p in L~ f

proof end;

theorem :: SPPOL_2:16

for f being FinSequence of (TOP-REAL 2)

for i being Nat st 1 <= i & i + 1 <= len f holds

LSeg ((f /. i),(f /. (i + 1))) c= L~ f

for i being Nat st 1 <= i & i + 1 <= len f holds

LSeg ((f /. i),(f /. (i + 1))) c= L~ f

proof end;

theorem :: SPPOL_2:17

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2)

for i being Nat st p in LSeg (f,i) holds

p in L~ f

for p being Point of (TOP-REAL 2)

for i being Nat st p in LSeg (f,i) holds

p in L~ f

proof end;

theorem Th19: :: SPPOL_2:19

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st not f is empty holds

L~ (f ^ <*p*>) = (L~ f) \/ (LSeg ((f /. (len f)),p))

for p being Point of (TOP-REAL 2) st not f is empty holds

L~ (f ^ <*p*>) = (L~ f) \/ (LSeg ((f /. (len f)),p))

proof end;

theorem Th20: :: SPPOL_2:20

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st not f is empty holds

L~ (<*p*> ^ f) = (LSeg (p,(f /. 1))) \/ (L~ f)

for p being Point of (TOP-REAL 2) st not f is empty holds

L~ (<*p*> ^ f) = (LSeg (p,(f /. 1))) \/ (L~ f)

proof end;

theorem Th23: :: SPPOL_2:23

for f1, f2 being FinSequence of (TOP-REAL 2) st not f1 is empty & not f2 is empty holds

L~ (f1 ^ f2) = ((L~ f1) \/ (LSeg ((f1 /. (len f1)),(f2 /. 1)))) \/ (L~ f2)

L~ (f1 ^ f2) = ((L~ f1) \/ (LSeg ((f1 /. (len f1)),(f2 /. 1)))) \/ (L~ f2)

proof end;

Lm1: for f being FinSequence of (TOP-REAL 2)

for n being Nat holds L~ (f | n) c= L~ f

proof end;

theorem Th24: :: SPPOL_2:24

for f being FinSequence of (TOP-REAL 2)

for q being Point of (TOP-REAL 2) st q in rng f holds

L~ f = (L~ (f -: q)) \/ (L~ (f :- q))

for q being Point of (TOP-REAL 2) st q in rng f holds

L~ f = (L~ (f -: q)) \/ (L~ (f :- q))

proof end;

theorem Th25: :: SPPOL_2:25

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2)

for n being Nat st p in LSeg (f,n) holds

L~ f = L~ (Ins (f,n,p))

for p being Point of (TOP-REAL 2)

for n being Nat st p in LSeg (f,n) holds

L~ f = L~ (Ins (f,n,p))

proof end;

registration

ex b_{1} being FinSequence of (TOP-REAL 2) st b_{1} is being_S-Seq

for b_{1} being FinSequence of (TOP-REAL 2) st b_{1} is being_S-Seq holds

( b_{1} is one-to-one & b_{1} is unfolded & b_{1} is s.n.c. & b_{1} is special & not b_{1} is trivial )
by NAT_D:60;

for b_{1} being FinSequence of (TOP-REAL 2) st b_{1} is one-to-one & b_{1} is unfolded & b_{1} is s.n.c. & b_{1} is special & not b_{1} is trivial holds

b_{1} is being_S-Seq
by NAT_D:60;

coherence

for b_{1} being FinSequence of (TOP-REAL 2) st b_{1} is being_S-Seq holds

not b_{1} is empty
;

end;

cluster V4() V7( NAT ) V8( the carrier of (TOP-REAL 2)) Function-like V38() FinSequence-like FinSubsequence-like being_S-Seq for FinSequence of the carrier of (TOP-REAL 2);

existence ex b

proof end;

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

coherence for b

( b

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

coherence for b

b

coherence

for b

not b

registration

ex b_{1} being FinSequence of (TOP-REAL 2) st

( b_{1} is one-to-one & b_{1} is unfolded & b_{1} is s.n.c. & b_{1} is special & not b_{1} is trivial )
end;

cluster V4() V7( NAT ) V8( the carrier of (TOP-REAL 2)) non trivial Function-like one-to-one V38() FinSequence-like FinSubsequence-like special unfolded s.n.c. for FinSequence of the carrier of (TOP-REAL 2);

existence ex b

( b

proof end;

Lm2: for p, q being Point of (TOP-REAL 2) holds <*p,q*> is unfolded

proof end;

Lm3: for f being FinSequence of (TOP-REAL 2)

for n being Nat st f is unfolded holds

f | n is unfolded

proof end;

Lm4: for f being FinSequence of (TOP-REAL 2)

for n being Nat st f is unfolded holds

f /^ n is unfolded

proof end;

registration

let f be unfolded FinSequence of (TOP-REAL 2);

let n be Nat;

coherence

for b_{1} being FinSequence of (TOP-REAL 2) st b_{1} = f | n holds

b_{1} is unfolded
by Lm3;

coherence

for b_{1} being FinSequence of (TOP-REAL 2) st b_{1} = f /^ n holds

b_{1} is unfolded
by Lm4;

end;
let n be Nat;

coherence

for b

b

coherence

for b

b

theorem Th27: :: SPPOL_2:27

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st p in rng f & f is unfolded holds

f :- p is unfolded

for p being Point of (TOP-REAL 2) st p in rng f & f is unfolded holds

f :- p is unfolded

proof end;

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

proof end;

registration

let f be unfolded FinSequence of (TOP-REAL 2);

let p be Point of (TOP-REAL 2);

coherence

f -: p is unfolded by Lm5;

end;
let p be Point of (TOP-REAL 2);

coherence

f -: p is unfolded by Lm5;

theorem Th29: :: SPPOL_2:29

for g being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st g is unfolded & (LSeg (p,(g /. 1))) /\ (LSeg (g,1)) = {(g /. 1)} holds

<*p*> ^ g is unfolded

for p being Point of (TOP-REAL 2) st g is unfolded & (LSeg (p,(g /. 1))) /\ (LSeg (g,1)) = {(g /. 1)} holds

<*p*> ^ g is unfolded

proof end;

theorem Th30: :: SPPOL_2:30

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2)

for k being Nat st f is unfolded & k + 1 = len f & (LSeg (f,k)) /\ (LSeg ((f /. (len f)),p)) = {(f /. (len f))} holds

f ^ <*p*> is unfolded

for p being Point of (TOP-REAL 2)

for k being Nat st f is unfolded & k + 1 = len f & (LSeg (f,k)) /\ (LSeg ((f /. (len f)),p)) = {(f /. (len f))} holds

f ^ <*p*> is unfolded

proof end;

theorem Th31: :: SPPOL_2:31

for f, g being FinSequence of (TOP-REAL 2)

for k being Nat st f is unfolded & g is unfolded & k + 1 = len f & (LSeg (f,k)) /\ (LSeg ((f /. (len f)),(g /. 1))) = {(f /. (len f))} & (LSeg ((f /. (len f)),(g /. 1))) /\ (LSeg (g,1)) = {(g /. 1)} holds

f ^ g is unfolded

for k being Nat st f is unfolded & g is unfolded & k + 1 = len f & (LSeg (f,k)) /\ (LSeg ((f /. (len f)),(g /. 1))) = {(f /. (len f))} & (LSeg ((f /. (len f)),(g /. 1))) /\ (LSeg (g,1)) = {(g /. 1)} holds

f ^ g is unfolded

proof end;

theorem Th32: :: SPPOL_2:32

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2)

for n being Nat st f is unfolded & p in LSeg (f,n) holds

Ins (f,n,p) is unfolded

for p being Point of (TOP-REAL 2)

for n being Nat st f is unfolded & p in LSeg (f,n) holds

Ins (f,n,p) is unfolded

proof end;

Lm6: for p, q being Point of (TOP-REAL 2) holds <*p,q*> is s.n.c.

proof end;

Lm7: for f being FinSequence of (TOP-REAL 2)

for n being Nat st f is s.n.c. holds

f | n is s.n.c.

proof end;

Lm8: for f being FinSequence of (TOP-REAL 2)

for n being Nat st f is s.n.c. holds

f /^ n is s.n.c.

proof end;

registration

let f be s.n.c. FinSequence of (TOP-REAL 2);

let n be Nat;

coherence

for b_{1} being FinSequence of (TOP-REAL 2) st b_{1} = f | n holds

b_{1} is s.n.c.
by Lm7;

coherence

for b_{1} being FinSequence of (TOP-REAL 2) st b_{1} = f /^ n holds

b_{1} is s.n.c.
by Lm8;

end;
let n be Nat;

coherence

for b

b

coherence

for b

b

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.

proof end;

registration

let f be s.n.c. FinSequence of (TOP-REAL 2);

let p be Point of (TOP-REAL 2);

coherence

f -: p is s.n.c. by Lm9;

end;
let p be Point of (TOP-REAL 2);

coherence

f -: p is s.n.c. by Lm9;

theorem Th34: :: SPPOL_2:34

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st p in rng f & f is s.n.c. holds

f :- p is s.n.c.

for p being Point of (TOP-REAL 2) st p in rng f & f is s.n.c. holds

f :- p is s.n.c.

proof end;

theorem Th36: :: SPPOL_2:36

for f, g being FinSequence of (TOP-REAL 2) st f is s.n.c. & g is s.n.c. & L~ f misses L~ g & ( for i being Nat st 1 <= i & i + 2 <= len f holds

LSeg (f,i) misses LSeg ((f /. (len f)),(g /. 1)) ) & ( for i being Nat st 2 <= i & i + 1 <= len g holds

LSeg (g,i) misses LSeg ((f /. (len f)),(g /. 1)) ) holds

f ^ g is s.n.c.

LSeg (f,i) misses LSeg ((f /. (len f)),(g /. 1)) ) & ( for i being Nat st 2 <= i & i + 1 <= len g holds

LSeg (g,i) misses LSeg ((f /. (len f)),(g /. 1)) ) holds

f ^ g is s.n.c.

proof end;

theorem Th37: :: SPPOL_2:37

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2)

for n being Nat st f is unfolded & f is s.n.c. & p in LSeg (f,n) & not p in rng f holds

Ins (f,n,p) is s.n.c.

for p being Point of (TOP-REAL 2)

for n being Nat st f is unfolded & f is s.n.c. & p in LSeg (f,n) & not p in rng f holds

Ins (f,n,p) is s.n.c.

proof end;

registration

let p be Point of (TOP-REAL 2);

coherence

for b_{1} being FinSequence of (TOP-REAL 2) st b_{1} = <*p*> holds

b_{1} is special

end;
coherence

for b

b

proof end;

Lm10: for f being FinSequence of (TOP-REAL 2)

for n being Nat st f is special holds

f | n is special

proof end;

Lm11: for f being FinSequence of (TOP-REAL 2)

for n being Nat st f is special holds

f /^ n is special

proof end;

registration

let f be special FinSequence of (TOP-REAL 2);

let n be Nat;

coherence

for b_{1} being FinSequence of (TOP-REAL 2) st b_{1} = f | n holds

b_{1} is special
by Lm10;

coherence

for b_{1} being FinSequence of (TOP-REAL 2) st b_{1} = f /^ n holds

b_{1} is special
by Lm11;

end;
let n be Nat;

coherence

for b

b

coherence

for b

b

theorem Th39: :: SPPOL_2:39

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st p in rng f & f is special holds

f :- p is special

for p being Point of (TOP-REAL 2) st p in rng f & f is special holds

f :- p is special

proof end;

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

proof end;

registration

let f be special FinSequence of (TOP-REAL 2);

let p be Point of (TOP-REAL 2);

coherence

f -: p is special by Lm12;

end;
let p be Point of (TOP-REAL 2);

coherence

f -: p is special by Lm12;

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

proof end;

theorem Th41: :: SPPOL_2:41

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2)

for n being Nat st f is special & p in LSeg (f,n) holds

Ins (f,n,p) is special

for p being Point of (TOP-REAL 2)

for n being Nat st f is special & p in LSeg (f,n) holds

Ins (f,n,p) is special

proof end;

theorem Th42: :: SPPOL_2:42

for f being FinSequence of (TOP-REAL 2)

for q being Point of (TOP-REAL 2) st q in rng f & 1 <> q .. f & q .. f <> len f & f is unfolded & f is s.n.c. holds

(L~ (f -: q)) /\ (L~ (f :- q)) = {q}

for q being Point of (TOP-REAL 2) st q in rng f & 1 <> q .. f & q .. f <> len f & f is unfolded & f is s.n.c. holds

(L~ (f -: q)) /\ (L~ (f :- q)) = {q}

proof end;

registration

let f be S-Sequence_in_R2;

coherence

for b_{1} being FinSequence of (TOP-REAL 2) st b_{1} = Rev f holds

b_{1} is being_S-Seq

end;
coherence

for b

b

proof end;

theorem :: SPPOL_2:45

for p, q being Point of (TOP-REAL 2) st p <> q & ( p `1 = q `1 or p `2 = q `2 ) holds

LSeg (p,q) is being_S-P_arc

LSeg (p,q) is being_S-P_arc

proof end;

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

proof end;

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

proof end;

theorem Th46: :: SPPOL_2:46

for p being Point of (TOP-REAL 2)

for f being S-Sequence_in_R2 st p in rng f & p .. f <> 1 holds

f -: p is being_S-Seq

for f being S-Sequence_in_R2 st p in rng f & p .. f <> 1 holds

f -: p is being_S-Seq

proof end;

theorem :: SPPOL_2:47

for p being Point of (TOP-REAL 2)

for f being S-Sequence_in_R2 st p in rng f & p .. f <> len f holds

f :- p is being_S-Seq

for f being S-Sequence_in_R2 st p in rng f & p .. f <> len f holds

f :- p is being_S-Seq

proof end;

theorem Th48: :: SPPOL_2:48

for p being Point of (TOP-REAL 2)

for i being Nat

for f being S-Sequence_in_R2 st p in LSeg (f,i) & not p in rng f holds

Ins (f,i,p) is being_S-Seq

for i being Nat

for f being S-Sequence_in_R2 st p in LSeg (f,i) & not p in rng f holds

Ins (f,i,p) is being_S-Seq

proof end;

registration
end;

theorem :: SPPOL_2:49

for P being Subset of (TOP-REAL 2)

for p1, p2 being Point of (TOP-REAL 2) st P is_S-P_arc_joining p1,p2 holds

P is_S-P_arc_joining p2,p1

for p1, p2 being Point of (TOP-REAL 2) st P is_S-P_arc_joining p1,p2 holds

P is_S-P_arc_joining p2,p1

proof end;

:: deftheorem 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) ) ) );

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 Th50: :: SPPOL_2:50

for P being Subset of (TOP-REAL 2)

for p1, p2 being Point of (TOP-REAL 2) st p1,p2 split P holds

p2,p1 split P

for p1, p2 being Point of (TOP-REAL 2) st p1,p2 split P holds

p2,p1 split P

proof end;

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) )

proof end;

theorem Th51: :: SPPOL_2:51

for P being Subset of (TOP-REAL 2)

for p1, p2, q being Point of (TOP-REAL 2) st p1,p2 split P & q in P & q <> p1 holds

p1,q split P

for p1, p2, q being Point of (TOP-REAL 2) st p1,p2 split P & q in P & q <> p1 holds

p1,q split P

proof end;

theorem Th52: :: SPPOL_2:52

for P being Subset of (TOP-REAL 2)

for p1, p2, q being Point of (TOP-REAL 2) st p1,p2 split P & q in P & q <> p2 holds

q,p2 split P

for p1, p2, q being Point of (TOP-REAL 2) st p1,p2 split P & q in P & q <> p2 holds

q,p2 split P

proof end;

theorem Th53: :: SPPOL_2:53

for P being Subset of (TOP-REAL 2)

for p1, p2, q1, q2 being Point of (TOP-REAL 2) st p1,p2 split P & q1 in P & q2 in P & q1 <> q2 holds

q1,q2 split P

for p1, p2, q1, q2 being Point of (TOP-REAL 2) st p1,p2 split P & q1 in P & q2 in P & q1 <> q2 holds

q1,q2 split P

proof end;

notation
end;

definition

let P be Subset of (TOP-REAL 2);

( P is special_polygonal iff ex p1, p2 being Point of (TOP-REAL 2) st p1,p2 split P )

end;
redefine attr P is being_special_polygon means :: SPPOL_2:def 2

ex p1, p2 being Point of (TOP-REAL 2) st p1,p2 split P;

compatibility ex p1, p2 being Point of (TOP-REAL 2) st p1,p2 split P;

( P is special_polygonal iff ex p1, p2 being Point of (TOP-REAL 2) st p1,p2 split P )

proof end;

:: deftheorem 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 );

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 );

definition

let r1, r2, r19, r29 be Real;

((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;
func [.r1,r2,r19,r29.] -> Subset of (TOP-REAL 2) equals :: SPPOL_2:def 3

((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]|)));

((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) ;

:: deftheorem defines [. SPPOL_2:def 3 :

for r1, r2, r19, r29 being Real 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]|)));

for r1, r2, r19, r29 being Real 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
end;

registration

let r1, r2, r19, r29 be Real;

coherence

( not [.r1,r2,r19,r29.] is empty & [.r1,r2,r19,r29.] is compact )

end;
coherence

( not [.r1,r2,r19,r29.] is empty & [.r1,r2,r19,r29.] is compact )

proof end;

theorem :: SPPOL_2:54

for r1, r2, r19, r29 being Real st r1 <= r2 & r19 <= r29 holds

[.r1,r2,r19,r29.] = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = r1 & p `2 <= r29 & p `2 >= r19 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r29 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r19 ) or ( p `1 = r2 & p `2 <= r29 & p `2 >= r19 ) ) }

[.r1,r2,r19,r29.] = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = r1 & p `2 <= r29 & p `2 >= r19 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r29 ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r19 ) or ( p `1 = r2 & p `2 <= r29 & p `2 >= r19 ) ) }

proof end;

theorem Th55: :: SPPOL_2:55

for r1, r2, r19, r29 being Real st r1 <> r2 & r19 <> r29 holds

[.r1,r2,r19,r29.] is special_polygonal

[.r1,r2,r19,r29.] is special_polygonal

proof end;

registration
end;

registration

existence

ex b_{1} being Subset of (TOP-REAL 2) st b_{1} is special_polygonal
by Th56;

coherence

for b_{1} being Subset of (TOP-REAL 2) st b_{1} is special_polygonal holds

not b_{1} is empty
;

coherence

for b_{1} being Subset of (TOP-REAL 2) st b_{1} is special_polygonal holds

not b_{1} is trivial
by ZFMISC_1:def 10;

end;
ex b

coherence

for b

not b

coherence

for b

not b

theorem :: SPPOL_2:59

for P being Subset of (TOP-REAL 2) st P is special_polygonal holds

for p1, p2 being Point of (TOP-REAL 2) st p1 <> p2 & p1 in P & p2 in P holds

ex P1, P2 being Subset of (TOP-REAL 2) st

( P1 is_S-P_arc_joining p1,p2 & P2 is_S-P_arc_joining p1,p2 & P1 /\ P2 = {p1,p2} & P = P1 \/ P2 )

for p1, p2 being Point of (TOP-REAL 2) st p1 <> p2 & p1 in P & p2 in P holds

ex P1, P2 being Subset of (TOP-REAL 2) st

( P1 is_S-P_arc_joining p1,p2 & P2 is_S-P_arc_joining p1,p2 & P1 /\ P2 = {p1,p2} & P = P1 \/ P2 )

proof end;