environ
vocabularies HIDDEN, NUMBERS, NAT_1, XREAL_0, PROB_1, FINSEQ_1, ZFMISC_1, XBOOLE_0, CARD_1, ARYTM_3, XXREAL_0, ARYTM_1, RELAT_1, SEQ_1, FUNCT_1, SEQ_2, ORDINAL2, SUBSET_1, COMPLEX1, RPR_1, TARSKI, VALUED_0, EQREL_1, CARD_3, PROB_2, SERIES_1, XXREAL_2, FINSEQ_2, SETFAM_1, BINOP_2, SETWISEO, FINSOP_1, SEQM_3, SETLIM_2, PROB_3, SEQ_4, REAL_1;
notations HIDDEN, FINSEQ_1, ORDINAL1, CARD_3, REAL_1, RELAT_1, TARSKI, XBOOLE_0, RVSUM_1, FINSOP_1, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, SETFAM_1, BINOP_1, SETWOP_2, BINOP_2, SETWISEO, NAT_1, FINSEQ_2, COMPLEX1, SEQ_1, COMSEQ_2, SEQ_2, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, PROB_1, PROB_2, KURATO_0, SETLIM_2, SEQM_3, SETLIM_1, RINFSUP1, SERIES_1, XXREAL_0;
definitions TARSKI, XBOOLE_0, RELAT_1, FINSEQ_1;
theorems FUNCT_1, FUNCT_2, SEQ_1, ABSVALUE, SEQ_2, SUBSET_1, NAT_1, TARSKI, XBOOLE_0, XBOOLE_1, PROB_2, SETLIM_2, RINFSUP1, RELAT_1, SETFAM_1, ZFMISC_1, SEQM_3, CARD_3, SETLIM_1, PROB_1, FINSUB_1, SERIES_1, FINSEQ_1, FINSEQ_2, FINSEQ_3, RVSUM_1, FINSOP_1, SETWISEO, BINOP_2, XREAL_1, XXREAL_0, ORDINAL1, VALUED_0, FUNCOP_1, XREAL_0;
schemes CLASSES1, NAT_1, RECDEF_1, FINSEQ_2, PARTFUN1;
registrations SUBSET_1, ORDINAL1, RELSET_1, NUMBERS, XREAL_0, NAT_1, PROB_1, VALUED_0, SEQ_2, FUNCT_2;
constructors HIDDEN, SETFAM_1, PARTFUN1, SETWISEO, XXREAL_0, REAL_1, NAT_1, BINOP_2, COMPLEX1, SEQ_2, SEQM_3, PROB_2, FINSOP_1, RVSUM_1, SERIES_1, BINOP_1, KURATO_0, SETLIM_1, RINFSUP1, SETLIM_2, PROB_1, RELSET_1, SETWOP_2, COMSEQ_2;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities XBOOLE_0, FINSEQ_2;
expansions TARSKI, XBOOLE_0, RELAT_1, FUNCT_2;
Lm1:
for t, p, s being Real st 0 < s & t <= p holds
( t < p + s & t - s < p )