environ
vocabularies HIDDEN, NUMBERS, SUPINF_1, SUBSET_1, TARSKI, XXREAL_1, ARYTM_3, XXREAL_0, CARD_1, XXREAL_2, ORDINAL2, REAL_1, SUPINF_2, MEMBERED, ARYTM_1, XBOOLE_0, MEASURE5, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, MEMBERED, XXREAL_0, XREAL_0, REAL_1, XXREAL_1, RCOMP_1, XXREAL_2, SUPINF_1, SUPINF_2;
definitions MEMBERED, XBOOLE_0;
theorems TARSKI, XREAL_0, XBOOLE_0, XREAL_1, XXREAL_0, NUMBERS, XXREAL_1, XXREAL_2, XXREAL_3;
schemes ;
registrations XBOOLE_0, NUMBERS, XXREAL_0, XREAL_0, MEMBERED, XXREAL_1, XXREAL_2, SUBSET_1, FINSET_1, ORDINAL1;
constructors HIDDEN, DOMAIN_1, REAL_1, RCOMP_1, SUPINF_2, SUPINF_1, FINSET_1;
requirements HIDDEN, SUBSET, BOOLE, NUMERALS, ARITHM, REAL;
equalities XXREAL_1, XXREAL_3;
expansions ;
scheme
RSetEq{
P1[
set ] } :
for
X1,
X2 being
Subset of
REAL st ( for
x being
R_eal holds
(
x in X1 iff
P1[
x] ) ) & ( for
x being
R_eal holds
(
x in X2 iff
P1[
x] ) ) holds
X1 = X2
Lm1:
for A being Interval holds diameter A >= 0
Lm2:
for A, B being Interval st A c= B holds
diameter A <= diameter B