environ
vocabularies HIDDEN, NUMBERS, RLVECT_1, ALGSTR_1, XBOOLE_0, ALGSTR_0, STRUCT_0, VECTSP_2, VECTSP_1, BINOP_1, LATTICES, ZFMISC_1, SUBSET_1, CARD_3, FINSEQ_1, ARYTM_3, ORDINAL4, RELAT_1, CARD_FIL, SUPINF_2, TARSKI, ARYTM_1, MESFUNC1, CARD_1, NEWTON, NAT_1, XXREAL_0, REALSET1, FUNCT_1, FUNCT_7, GROUP_1, PARTFUN1, PRELAMB, MCART_1, SETFAM_1, RLVECT_3, GCD_1, LATTICE3, SQUARE_1, FINSET_1, INT_3, XCMPLX_0, IDEAL_1, RECDEF_2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSET_1, RELAT_1, FUNCT_1, FINSEQ_1, ORDINAL1, REALSET1, INT_3, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, RELSET_1, PARTFUN1, FUNCT_2, ALGSTR_1, XXREAL_2, XTUPLE_0, MCART_1, POLYNOM1, SETFAM_1, DOMAIN_1, FINSEQ_4, NEWTON, STRUCT_0, ALGSTR_0, RLVECT_1, VECTSP_1, GROUP_1, BINOP_1, VECTSP_2, FUNCT_7, GCD_1, BINOM;
definitions TARSKI, XBOOLE_0, ALGSTR_0;
theorems INT_3, TARSKI, ZFMISC_1, RLVECT_1, VECTSP_1, GCD_1, FUNCT_1, FUNCT_2, POLYNOM1, RELAT_1, FINSET_1, NAT_1, ALGSTR_1, FINSEQ_1, FINSEQ_2, FINSEQ_3, SETFAM_1, INT_1, FINSEQ_4, FINSEQ_5, POLYNOM2, BINOM, XBOOLE_0, XBOOLE_1, ORDINAL1, GROUP_1, XREAL_1, DOMAIN_1, XXREAL_0, PARTFUN1, XXREAL_2, SUBSET_1, CARD_1;
schemes NAT_1, RECDEF_1, FUNCT_2, FINSEQ_2, DOMAIN_1, INT_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_2, FINSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED, FINSEQ_1, REALSET1, STRUCT_0, VECTSP_1, ALGSTR_1, INT_3, VALUED_0, ALGSTR_0, XXREAL_2, CARD_1, RELSET_1, XTUPLE_0, ORDINAL1;
constructors HIDDEN, SETFAM_1, BINOP_1, REALSET2, ALGSTR_1, GCD_1, INT_3, POLYNOM1, BINOM, XXREAL_2, RELSET_1, FUNCT_7, FVSUM_1, FINSEQ_4, XTUPLE_0, NEWTON;
requirements HIDDEN, NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
equalities CARD_1, BINOP_1, REALSET1, STRUCT_0, ALGSTR_0, ORDINAL1;
expansions TARSKI, XBOOLE_0;
Lm1:
for R being comRing
for a being Element of R holds { (a * r) where r is Element of R : verum } is Ideal of R
Lm2:
for a, b being set holds {a} c= {a,b}