environ
vocabularies HIDDEN, SUBSET_1, LATTICES, LATSTONE, XBOOLE_0, TARSKI, EQREL_1, PBOOLE, ORDINAL4, XXREAL_2, STRUCT_0, ZFMISC_1, LATTICE5, FILTER_0, LATTICE4, TOPS_1, REWRITE1, MOEBIUS2, NAT_1, FINSET_1, XCMPLX_0, MOEBIUS1, RELAT_1, BINOP_1, REALSET1, LATTICEA, XXREAL_0, CARD_1, NUMBERS, NEWTON, ARYTM_3;
notations HIDDEN, TARSKI, ZFMISC_1, XBOOLE_0, RELAT_1, ORDINAL1, NAT_1, FINSET_1, ARYTM_3, BINOP_1, REALSET1, SUBSET_1, NAT_D, ENUMSET1, XCMPLX_0, XXREAL_0, CARD_1, NUMBERS, NEWTON, INT_2, FUNCT_1, FUNCT_2, STRUCT_0, LATTICES, LATTICE3, FILTER_0, FILTER_1, FILTER_2, LATTICE4, MOEBIUS1, MOEBIUS2, LATTICEA;
definitions TARSKI, XBOOLE_0, LATTICES;
theorems LATTICES, FILTER_0, FILTER_2, MSUALG_7, MOEBIUS2, MOEBIUS1, NEWTON, ENUMSET1, INT_2, NAT_5, TARSKI, BOOLEALG, FILTER_1, ZFMISC_1, XTUPLE_0, LATTICEA, LATTICE4;
schemes ;
registrations STRUCT_0, LATTICES, PARTFUN1, FUNCT_2, REALSET1, INT_1, FILTER_1, LATTICE3, MOEBIUS1, MOEBIUS2, XCMPLX_0, CARD_1, INT_2, INT_3, NEWTON, NAT_1, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XREAL_0, RELSET_1, PBOOLE, LATTICE6;
constructors HIDDEN, DOMAIN_1, XBOOLE_0, FILTER_1, NAT_1, ORDINAL1, INT_2, NEWTON, ARYTM_3, NAT_D, SQUARE_1, ENUMSET1, ZFMISC_1, FILTER_0, FINSET_1, FILTER_2, LATTICE4, MOEBIUS1, XREAL_0, XCMPLX_0, XXREAL_0, BINOP_1, REALSET2, LATTICE3, PARTFUN1, MOEBIUS2, SUBSET_1, BOOLEALG, REALSET1, LATTICEA;
requirements HIDDEN, SUBSET, BOOLE, REAL, NUMERALS, ARITHM;
equalities FILTER_1;
expansions ;
LattIsComplemented:
for L being Stone Lattice holds latt (L,(Skeleton L)) is complemented
:: for the paper of Jouni J\"arvinen "Lattice theory for rough sets",
:: in Transactions of Rough Sets, VI, LNCS vol. 4374, pp. 400--498, 2007.
:: The corresponding items are marked by the acronym LTRS. We deal
:: with Section 4.3, page 423--426.