environ
vocabularies HIDDEN, RLSUB_1, HAHNBAN, UNIALG_1, DUALSP01, DUALSP02, DUALSP03, PBOOLE, INT_1, NFCONT_1, CFCONT_1, RLVECT_1, ARYTM_1, RELAT_1, FUNCT_1, RSSPACE, RSSPACE3, REAL_1, TARSKI, MSSUBFAM, STRUCT_0, SEQ_1, FUNCOP_1, FCONT_1, SEQ_2, LOPBAN_1, ORDINAL2, ARYTM_3, NORMSP_1, FUNCT_2, PRE_TOPC, SUBSET_1, ZFMISC_1, NUMBERS, SEQ_4, XBOOLE_0, CARD_1, SUPINF_2, COMPLEX1, XXREAL_0, XXREAL_2, NAT_1, REWRITE1, VALUED_1, METRIC_1, ASYMPT_1, PARTFUN1, RCOMP_1, NORMSP_2, RLVECT_3, NORMSP_3, TOPS_1, TOPGEN_1, VALUED_0;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, INT_1, VALUED_0, COMPLEX1, XXREAL_2, VALUED_1, SEQ_1, SEQ_2, SEQ_4, RINFSUP1, STRUCT_0, PRE_TOPC, TOPS_1, RLVECT_1, RLSUB_1, RLVECT_3, NORMSP_0, NORMSP_1, HAHNBAN, RSSPACE, RSSPACE3, LOPBAN_1, NFCONT_1, NORMSP_2, LOPBAN_5, DUALSP01, NORMSP_3, DUALSP02;
definitions HAHNBAN, TARSKI;
theorems SEQ_4, FUNCT_1, SEQ_1, SEQ_2, ABSVALUE, COMPLEX1, TARSKI, RSSPACE3, XREAL_0, XXREAL_0, NORMSP_1, LOPBAN_1, FUNCT_2, XBOOLE_0, XREAL_1, RLVECT_1, FUNCOP_1, HAHNBAN, NORMSP_0, ORDINAL1, NAT_1, NORMSP_3, INT_1, NFCONT_1, XXREAL_2, SEQM_3, DUALSP01, RELAT_1, XCMPLX_1, NORMSP_2, BINOP_2, NUMBERS, LOPBAN_5, RLVECT_3, VALUED_0, DUALSP02, RINFSUP1, EUCLID, NORMSP_4;
schemes FUNCT_2, RECDEF_1, NAT_1, RECDEF_2;
registrations STRUCT_0, XREAL_0, NUMBERS, ORDINAL1, MEMBERED, RELAT_1, XXREAL_0, VALUED_0, FUNCT_2, VALUED_1, FUNCOP_1, SEQ_4, RELSET_1, FUNCT_1, NORMSP_3, DUALSP02, XCMPLX_0, NORMSP_0, NAT_1, NORMSP_1, SEQ_2, DUALSP01, XBOOLE_0, SEQM_3, INT_1, LOPBAN_1, PRE_TOPC, NORMSP_4;
constructors HIDDEN, REAL_1, EUCLID, REALSET1, RSSPACE3, BINOP_2, SEQ_1, NFCONT_1, RELSET_1, SEQ_2, SEQ_4, HAHNBAN1, NORMSP_2, RLVECT_3, LOPBAN_5, COMSEQ_2, NORMSP_3, TOPS_1, DUALSP02, RINFSUP1, CARD_3;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
equalities STRUCT_0, ALGSTR_0, NORMSP_0, SEQ_1, DUALSP02, DUALSP01;
expansions TARSKI, XBOOLE_0, FUNCT_2, SEQ_2, NORMSP_1, STRUCT_0, NORMSP_3, SEQM_3, XXREAL_2, NFCONT_1, DUALSP01;
Th713A:
for X being RealBanachSpace
for X0 being non empty Subset of X st not X is trivial & X is Reflexive & X0 is weakly-sequentially-compact holds
ex S being non empty Subset of REAL st
( S = { ||.x.|| where x is Point of X : x in X0 } & S is bounded_above )