environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, FUNCT_1, TARSKI, RELAT_1, SUBSET_1, VALUED_0, PARTFUN1, FUNCT_2, MEMBERED, XCMPLX_0, ARYTM_3, ARYTM_1, VALUED_1, RAT_1, FINSEQ_1, NAT_1, COMPLEX1, INT_1, VALUED_2, FUNCOP_1, REAL_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, ORDINAL1, NUMBERS, FUNCOP_1, BINOP_1, VALUED_0, VALUED_1, INT_1, NAT_1, XCMPLX_0, XREAL_0, RAT_1, MEMBERED, FINSEQ_1;
definitions TARSKI, FUNCT_1, FUNCOP_1;
theorems TARSKI, SUBSET_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, VALUED_1, XCMPLX_1, XBOOLE_0, XBOOLE_1, RFUNCT_1, FINSEQ_1, RELAT_1, ZFMISC_1, XCMPLX_0, XREAL_0, RAT_1, INT_1, ORDINAL1;
schemes XBOOLE_0, FUNCT_1, CLASSES1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, VALUED_0, VALUED_1, RELSET_1, MEMBERED, ORDINAL1, XCMPLX_0, NUMBERS, RAT_1, XREAL_0, INT_1;
constructors HIDDEN, RELAT_2, PARTFUN1, MCART_1, FUNCT_2, VALUED_0, VALUED_1, NAT_1, ARYTM_0, XCMPLX_0, FINSEQ_1, ARYTM_2, NUMBERS, XXREAL_0, XREAL_0, COMPLEX1, RELSET_1, FUNCOP_1, BINOP_1;
requirements HIDDEN, SUBSET, BOOLE, NUMERALS, ARITHM, REAL;
equalities XCMPLX_0, VALUED_1, BINOP_1, ORDINAL1;
expansions TARSKI;
Lm1:
now for X1, X2, X3 being set holds X1 /\ (X2 /\ X3) = (X1 /\ X2) /\ (X1 /\ X3)
end;
set ff = the natural-valued Function;