environ
vocabularies HIDDEN, SUBSET_1, PRE_TOPC, SETFAM_1, STRUCT_0, TARSKI, ZFMISC_1, XBOOLE_0, FUNCT_1, RELAT_1, RCOMP_1, XXREAL_0, CARD_1, QC_LANG1, ORDERS_2, WAYBEL_9, TOPS_1, FINSUB_1, ROUGHS_4, BINOP_1, WAYBEL_1, COHSP_1, ROUGHS_1, ROUGHS_2, ISOMICHI, FRECHET2, FRECHET, KURATO_1, ARYTM_1, TDLAT_3;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, SETFAM_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FINSUB_1, XXREAL_2, XXREAL_3, CARD_1, ENUMSET1, BINOP_1, FUNCT_2, FUNCT_3, XCMPLX_0, XREAL_0, NAT_1, RCOMP_1, FUNCOP_1, FINSEQ_1, STRUCT_0, PRE_TOPC, ORDERS_2, EQREL_1, TOPMETR, COHSP_1, TOPS_1, TDLAT_2, WAYBEL_9, ROUGHS_1, ROUGHS_2, ISOMICHI, FRECHET, FRECHET2, KURATO_1, TDLAT_3;
definitions TARSKI, FINSUB_1, ISOMICHI, TDLAT_3, ROUGHS_2;
theorems XBOOLE_1, PRE_TOPC, ZFMISC_1, SETFAM_1, TOPS_1, ROUGHS_1, ROUGHS_2, FUNCT_1, TARSKI, MEASURE1, ISOMICHI, FRECHET2, FRECHET, KURATO_1, ENUMSET1, CARD_2;
schemes FRAENKEL, SUBSET_1, XBOOLE_0, FUNCT_2;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FUNCT_2, STRUCT_0, PRE_TOPC, XREAL_0, FINSEQ_1, RELAT_1, FUNCT_1, ORDINAL1, NAT_1, TOPS_1, ORDERS_2, ROUGHS_1, ROUGHS_2, WAYBEL_9, PROB_1, ISOMICHI, FRECHET, KURATO_1, TDLAT_3, FINSET_1, YELLOW_3, TOPMETR, XXREAL_0;
constructors HIDDEN, SETFAM_1, PARTFUN1, FUNCT_3, XXREAL_0, XREAL_0, NAT_1, MEMBERED, XXREAL_1, XXREAL_2, XXREAL_3, FINSEQ_1, CONNSP_1, RELSET_1, NUMBERS, BINOP_1, COHSP_1, TDLAT_2, FUNCOP_1, ORDERS_2, FINSUB_1, EQREL_1, PCOMPS_1, PCOMPS_2, ROUGHS_1, ROUGHS_2, WAYBEL_9, TDLAT_3, TOPS_1, ISOMICHI, FRECHET, FRECHET2, KURATO_1, TOPMETR, RCOMP_1, MEASURE6;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities STRUCT_0, SUBSET_1, KURATO_1, ISOMICHI, TARSKI, XBOOLE_0, RELAT_1, FUNCT_2, ROUGHS_1;
expansions TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, RELAT_1, FUNCT_2, ROUGHS_1, WAYBEL_9, FINSUB_1, ISOMICHI, TDLAT_3, ROUGHS_2;
OpenLap:
for T being non empty with_equivalence naturally_generated TopRelStr
for A being open Subset of T holds LAp A = Int A
:: Cl_Seq from FRECHET2 is important example of preclosure