:: SPPOL_2 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: SPPOL_2:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r1, r2, r1', r2' being real number st |[r1,r2]| = |[r1',r2']| holds
( r1 = r1' & r2 = r2' )
proof end;

theorem Th2: :: SPPOL_2:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th3: :: SPPOL_2:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th4: :: SPPOL_2:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of (TOP-REAL 2)
for n, i being Nat st n <= len f & 1 <= i holds
LSeg (f /^ n),i = LSeg f,(n + i)
proof end;

theorem Th5: :: SPPOL_2:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th6: :: SPPOL_2:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th7: :: SPPOL_2:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th8: :: SPPOL_2:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th9: :: SPPOL_2:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th10: :: SPPOL_2:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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))
proof end;

theorem Th11: :: SPPOL_2:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
L~ (<*> the carrier of (TOP-REAL 2)) = {}
proof end;

theorem Th12: :: SPPOL_2:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Point of (TOP-REAL 2) holds L~ <*p*> = {}
proof end;

theorem Th13: :: SPPOL_2:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th14: :: SPPOL_2:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)) )
proof end;

theorem Th15: :: SPPOL_2:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: SPPOL_2:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: SPPOL_2:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th18: :: SPPOL_2:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of (TOP-REAL 2) st len f >= 2 holds
rng f c= L~ f
proof end;

theorem Th19: :: SPPOL_2:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th20: :: SPPOL_2:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th21: :: SPPOL_2:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Point of (TOP-REAL 2) holds L~ <*p,q*> = LSeg p,q
proof end;

theorem Th22: :: SPPOL_2:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of (TOP-REAL 2) holds L~ f = L~ (Rev f)
proof end;

theorem Th23: :: SPPOL_2:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
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 :: SPPOL_2:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th25: :: SPPOL_2:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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))
proof end;

theorem Th26: :: SPPOL_2:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

registration
cluster being_S-Seq FinSequence of the carrier of (TOP-REAL 2);
existence
ex b1 being FinSequence of (TOP-REAL 2) st b1 is being_S-Seq
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
for b1 being FinSequence of (TOP-REAL 2) st b1 is being_S-Seq holds
( b1 is one-to-one & b1 is unfolded & b1 is s.n.c. & b1 is special & not b1 is trivial )
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
for b1 being FinSequence of (TOP-REAL 2) st b1 is one-to-one & b1 is unfolded & b1 is s.n.c. & b1 is special & not b1 is trivial holds
b1 is being_S-Seq
proof end;
cluster being_S-Seq -> non empty FinSequence of the carrier of (TOP-REAL 2);
coherence
for b1 being FinSequence of (TOP-REAL 2) st b1 is being_S-Seq holds
not b1 is empty
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
ex b1 being FinSequence of (TOP-REAL 2) st
( b1 is one-to-one & b1 is unfolded & b1 is s.n.c. & b1 is special & not b1 is trivial )
proof end;
end;

theorem Th27: :: SPPOL_2:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of (TOP-REAL 2) st len f <= 2 holds
f is unfolded
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;
cluster f | n -> unfolded ;
coherence
f | n is unfolded
by Lm3;
cluster f /^ n -> unfolded ;
coherence
f /^ n is unfolded
by Lm4;
end;

theorem Th28: :: SPPOL_2:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
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);
cluster f -: p -> unfolded ;
coherence
f -: p is unfolded
by Lm5;
end;

theorem Th29: :: SPPOL_2:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of (TOP-REAL 2) st f is unfolded holds
Rev f is unfolded
proof end;

theorem Th30: :: SPPOL_2:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th31: :: SPPOL_2:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th32: :: SPPOL_2:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th33: :: SPPOL_2:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th34: :: SPPOL_2:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of (TOP-REAL 2) st len f <= 2 holds
f is s.n.c.
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;
cluster f | n -> s.n.c. ;
coherence
f | n is s.n.c.
by Lm7;
cluster f /^ n -> s.n.c. ;
coherence
f /^ n is s.n.c.
by Lm8;
end;

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);
cluster f -: p -> s.n.c. ;
coherence
f -: p is s.n.c.
by Lm9;
end;

theorem Th35: :: SPPOL_2:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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.
proof end;

theorem Th36: :: SPPOL_2:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of (TOP-REAL 2) st f is s.n.c. holds
Rev f is s.n.c.
proof end;

theorem Th37: :: SPPOL_2:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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.
proof end;

theorem Th38: :: SPPOL_2:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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.
proof end;

Lm10: <*> the carrier of (TOP-REAL 2) is special
proof end;

registration
cluster <*> the carrier of (TOP-REAL 2) -> special ;
coherence
<*> the carrier of (TOP-REAL 2) is special
by Lm10;
end;

theorem Th39: :: SPPOL_2:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Point of (TOP-REAL 2) holds <*p*> is special
proof end;

theorem Th40: :: SPPOL_2:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Point of (TOP-REAL 2) st ( p `1 = q `1 or p `2 = q `2 ) holds
<*p,q*> 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;

Lm12: 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;
cluster f | n -> special ;
coherence
f | n is special
by Lm11;
cluster f /^ n -> special ;
coherence
f /^ n is special
by Lm12;
end;

theorem Th41: :: SPPOL_2:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

Lm13: 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);
cluster f -: p -> special ;
coherence
f -: p is special
by Lm13;
end;

theorem Th42: :: SPPOL_2:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of (TOP-REAL 2) st f is special holds
Rev f is special
proof end;

Lm14: 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 :: SPPOL_2:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th44: :: SPPOL_2:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th45: :: SPPOL_2:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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}
proof end;

theorem Th46: :: SPPOL_2:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Point of (TOP-REAL 2) st p <> q & ( p `1 = q `1 or p `2 = q `2 ) holds
<*p,q*> 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being S-Sequence_in_R2 holds Rev f is being_S-Seq
proof end;

theorem :: SPPOL_2:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for f being S-Sequence_in_R2 st i in dom f holds
f /. i in L~ f
proof end;

theorem :: SPPOL_2:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
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;

Lm16: 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 Th50: :: SPPOL_2:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: SPPOL_2:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th52: :: SPPOL_2:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

registration
cluster being_S-P_arc Element of K40(the carrier of (TOP-REAL 2));
existence
ex b1 being Subset of (TOP-REAL 2) st b1 is being_S-P_arc
proof end;
end;

theorem :: SPPOL_2:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

definition
let p1, p2 be Point of (TOP-REAL 2);
let P be Subset of (TOP-REAL 2);
pred p1,p2 split P means :Def1: :: SPPOL_2:def 1
( 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) ) );
end;

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

theorem Th54: :: SPPOL_2:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

Lm17: 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 Th55: :: SPPOL_2:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th56: :: SPPOL_2:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th57: :: SPPOL_2:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

notation
let P be Subset of (TOP-REAL 2);
synonym special_polygonal P for being_special_polygon P;
end;

definition
let P be Subset of (TOP-REAL 2);
redefine attr P is being_special_polygon means :Def2: :: SPPOL_2:def 2
ex p1, p2 being Point of (TOP-REAL 2) st p1,p2 split P;
compatibility
( P is special_polygonal iff ex p1, p2 being Point of (TOP-REAL 2) st p1,p2 split P )
proof end;
end;

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

Lm18: for P being Subset of (TOP-REAL 2) st P is special_polygonal holds
ex p1, p2 being Point of (TOP-REAL 2) st
( p1 <> p2 & p1 in P & p2 in P )
proof end;

definition
let r1, r2, r1', r2' be real number ;
func [.r1,r2,r1',r2'.] -> Subset of (TOP-REAL 2) equals :: SPPOL_2:def 3
((LSeg |[r1,r1']|,|[r1,r2']|) \/ (LSeg |[r1,r2']|,|[r2,r2']|)) \/ ((LSeg |[r2,r2']|,|[r2,r1']|) \/ (LSeg |[r2,r1']|,|[r1,r1']|));
coherence
((LSeg |[r1,r1']|,|[r1,r2']|) \/ (LSeg |[r1,r2']|,|[r2,r2']|)) \/ ((LSeg |[r2,r2']|,|[r2,r1']|) \/ (LSeg |[r2,r1']|,|[r1,r1']|)) is Subset of (TOP-REAL 2)
;
end;

:: deftheorem defines [. SPPOL_2:def 3 :
for r1, r2, r1', r2' being real number holds [.r1,r2,r1',r2'.] = ((LSeg |[r1,r1']|,|[r1,r2']|) \/ (LSeg |[r1,r2']|,|[r2,r2']|)) \/ ((LSeg |[r2,r2']|,|[r2,r1']|) \/ (LSeg |[r2,r1']|,|[r1,r1']|));

registration
let n be Nat;
let p1, p2 be Point of (TOP-REAL n);
cluster LSeg p1,p2 -> compact ;
coherence
LSeg p1,p2 is compact
by SPPOL_1:28;
end;

registration
let r1, r2, r1', r2' be real number ;
cluster [.r1,r2,r1',r2'.] -> non empty compact ;
coherence
( not [.r1,r2,r1',r2'.] is empty & [.r1,r2,r1',r2'.] is compact )
proof end;
end;

theorem :: SPPOL_2:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r1, r2, r1', r2' being real number st r1 <= r2 & r1' <= r2' holds
[.r1,r2,r1',r2'.] = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = r1 & p `2 <= r2' & p `2 >= r1' ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r2' ) or ( p `1 <= r2 & p `1 >= r1 & p `2 = r1' ) or ( p `1 = r2 & p `2 <= r2' & p `2 >= r1' ) ) }
proof end;

theorem Th59: :: SPPOL_2:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r1, r2, r1', r2' being real number st r1 <> r2 & r1' <> r2' holds
[.r1,r2,r1',r2'.] is special_polygonal
proof end;

theorem Th60: :: SPPOL_2:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
R^2-unit_square = [.0,1,0,1.] ;

registration
cluster special_polygonal Element of K40(the carrier of (TOP-REAL 2));
existence
ex b1 being Subset of (TOP-REAL 2) st b1 is special_polygonal
proof end;
end;

theorem Th61: :: SPPOL_2:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
R^2-unit_square is special_polygonal by Th59, Th60;

registration
cluster special_polygonal Element of K40(the carrier of (TOP-REAL 2));
existence
ex b1 being Subset of (TOP-REAL 2) st b1 is special_polygonal
by Th61;
cluster special_polygonal -> non empty Element of K40(the carrier of (TOP-REAL 2));
coherence
for b1 being Subset of (TOP-REAL 2) st b1 is special_polygonal holds
not b1 is empty
proof end;
cluster special_polygonal -> non trivial Element of K40(the carrier of (TOP-REAL 2));
coherence
for b1 being Subset of (TOP-REAL 2) st b1 is special_polygonal holds
not b1 is trivial
proof end;
end;

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

theorem Th62: :: SPPOL_2:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Subset of (TOP-REAL 2) st P is being_S-P_arc holds
P is compact
proof end;

theorem :: SPPOL_2:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Special_polygon_in_R2 holds G is compact
proof end;

theorem Th64: :: SPPOL_2:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
p1,p2 split P
proof end;

theorem :: SPPOL_2:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;