environ
vocabularies HIDDEN, NUMBERS, PRE_TOPC, EUCLID, FINSEQ_1, SUBSET_1, RELAT_1, ARYTM_3, MCART_1, ARYTM_1, FUNCT_1, SQUARE_1, BINOP_2, COMPLEX1, RVSUM_1, CARD_3, NAT_1, STRUCT_0, REAL_1, XXREAL_0, RLTOPSP1, TARSKI, CARD_1, XBOOLE_0, TOPREAL1, PARTFUN1, ORDINAL4, METRIC_1, FINSEQ_2;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, SQUARE_1, COMPLEX1, REAL_1, NAT_1, RELAT_1, FUNCT_1, PARTFUN1, FINSEQ_1, BINOP_1, PRE_TOPC, FINSEQ_2, STRUCT_0, METRIC_1, RVSUM_1, RLVECT_1, RLTOPSP1, EUCLID, TOPREAL1, XXREAL_0;
definitions TARSKI, TOPREAL1, FUNCT_1, XBOOLE_0;
theorems TARSKI, NAT_1, ZFMISC_1, FUNCT_1, FINSEQ_1, ABSVALUE, SQUARE_1, FINSEQ_2, METRIC_1, RVSUM_1, EUCLID, TOPREAL1, FINSEQ_3, FINSEQ_4, PARTFUN2, TBSP_1, RELAT_1, INT_1, XBOOLE_0, XBOOLE_1, XCMPLX_1, XREAL_0, COMPLEX1, XREAL_1, BINOP_2, XXREAL_0, ORDINAL1, RLTOPSP1, RLVECT_1;
schemes ;
registrations RELSET_1, NUMBERS, XXREAL_0, XREAL_0, SQUARE_1, NAT_1, FINSEQ_1, STRUCT_0, EUCLID, VALUED_0, INT_1, ORDINAL1;
constructors HIDDEN, PARTFUN1, REAL_1, SQUARE_1, NAT_1, BINOP_2, COMPLEX1, FINSEQOP, FINSEQ_4, TOPREAL1, RVSUM_1, RELSET_1, DOMAIN_1, BINOP_1;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities TOPREAL1, XBOOLE_0, SQUARE_1, EUCLID, RVSUM_1, VALUED_1, ALGSTR_0, RLTOPSP1;
expansions TOPREAL1, FUNCT_1, XBOOLE_0;
theorem
for
p,
p1,
p2 being
Point of
(TOP-REAL 2) for
r,
r1,
r2,
s1,
s2 being
Real for
u being
Point of
(Euclid 2) st
u = p1 &
p1 = |[r1,s1]| &
p2 = |[r2,s2]| &
p = |[r2,s1]| &
p2 in Ball (
u,
r) holds
p in Ball (
u,
r)
theorem
for
r,
r1,
r2,
s1,
s2 being
Real for
u being
Point of
(Euclid 2) st
|[r1,r2]| in Ball (
u,
r) &
|[s1,s2]| in Ball (
u,
r) & not
|[r1,s2]| in Ball (
u,
r) holds
|[s1,r2]| in Ball (
u,
r)
theorem
for
p,
p1,
q being
Point of
(TOP-REAL 2) for
r being
Real for
u being
Point of
(Euclid 2) st not
p1 in Ball (
u,
r) &
p in Ball (
u,
r) &
|[(p `1),(q `2)]| in Ball (
u,
r) & not
|[(p `1),(q `2)]| in LSeg (
p1,
p) &
p1 `1 = p `1 &
p `1 <> q `1 &
p `2 <> q `2 holds
((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) = {p}
theorem
for
p,
p1,
q being
Point of
(TOP-REAL 2) for
r being
Real for
u being
Point of
(Euclid 2) st not
p1 in Ball (
u,
r) &
p in Ball (
u,
r) &
|[(q `1),(p `2)]| in Ball (
u,
r) & not
|[(q `1),(p `2)]| in LSeg (
p1,
p) &
p1 `2 = p `2 &
p `1 <> q `1 &
p `2 <> q `2 holds
((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p}