environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, EUCLID, FINSEQ_1, PRE_TOPC, NAT_1, ARYTM_3, RLTOPSP1, FINSEQ_5, XXREAL_0, RELAT_1, PARTFUN1, CARD_1, XBOOLE_0, RFINSEQ, ARYTM_1, ORDINAL4, FINSEQ_4, TOPREAL1, STRUCT_0, TARSKI, MCART_1, FUNCT_1, ZFMISC_1, TOPREAL4, XXREAL_1, RCOMP_1, BORSUK_1, TOPS_2, ORDINAL2, SPPOL_2, REAL_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, XXREAL_0, NAT_1, FUNCT_1, PARTFUN1, FINSEQ_1, ZFMISC_1, FINSEQ_4, RFINSEQ, STRUCT_0, PRE_TOPC, COMPTS_1, TOPS_2, RLTOPSP1, EUCLID, BORSUK_1, TOPREAL1, TOPREAL4, FINSEQ_5;
definitions TARSKI, TOPREAL1, TOPREAL4, XBOOLE_0;
theorems TARSKI, ENUMSET1, ZFMISC_1, NAT_1, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, TOPS_2, HEINE, TOPMETR, COMPTS_1, RFINSEQ, EUCLID, TOPREAL1, TOPREAL3, TOPREAL4, GOBOARD1, FINSEQ_5, RELAT_1, PARTFUN2, INT_1, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, ORDINAL1, PARTFUN1, RLTOPSP1, SEQ_4, NAT_D;
schemes FINSEQ_2;
registrations XBOOLE_0, RELAT_1, ORDINAL1, XREAL_0, FINSEQ_1, FINSEQ_5, STRUCT_0, PRE_TOPC, EUCLID, TOPREAL1, NAT_1, INT_1, CARD_1, RLTOPSP1, SPPOL_1;
constructors HIDDEN, XXREAL_0, NAT_1, FINSEQ_4, ZFMISC_1, RFINSEQ, BINARITH, FINSEQ_5, TOPS_2, COMPTS_1, TOPMETR, TOPREAL1, TOPREAL4, REAL_1, CONVEX1;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities TOPREAL1;
expansions TARSKI, TOPREAL1, TOPREAL4, XBOOLE_0;
Lm1:
for f being FinSequence of (TOP-REAL 2)
for n being Nat holds L~ (f | n) c= L~ f
Lm2:
for p, q being Point of (TOP-REAL 2) holds <*p,q*> is unfolded
Lm3:
for f being FinSequence of (TOP-REAL 2)
for n being Nat st f is unfolded holds
f | n is unfolded
Lm4:
for f being FinSequence of (TOP-REAL 2)
for n being Nat st f is unfolded holds
f /^ n is unfolded
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
Lm6:
for p, q being Point of (TOP-REAL 2) holds <*p,q*> is s.n.c.
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.
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.
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.
Lm10:
for f being FinSequence of (TOP-REAL 2)
for n being Nat st f is special holds
f | n is special
Lm11:
for f being FinSequence of (TOP-REAL 2)
for n being Nat st f is special holds
f /^ n is special
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
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
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
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
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) )
definition
let r1,
r2,
r19,
r29 be
Real;
func [.r1,r2,r19,r29.] -> Subset of
(TOP-REAL 2) equals
((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]|))) is Subset of (TOP-REAL 2)
;
end;
::
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]|)));