environ
vocabularies HIDDEN, NUMBERS, ORDERS_2, RELAT_1, NATTRA_1, TOLER_1, TARSKI, ZFMISC_1, MATRIX_1, STRUCT_0, RELAT_2, XBOOLE_0, PARTFUN1, SUBSET_1, FINSEQ_1, CARD_3, ORDINAL4, FUNCT_1, PROB_2, FINSEQ_2, NAT_1, FINSET_1, EQREL_1, CARD_1, ARYTM_3, XXREAL_0, XXREAL_1, FUNCT_3, ARYTM_1, ROUGHS_1, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, FINSET_1, RELAT_1, RELAT_2, FUNCT_1, FINSEQ_1, RVSUM_1, FINSEQ_2, RELSET_1, PARTFUN1, CARD_3, PROB_2, FUNCT_2, FUNCT_3, DOMAIN_1, STRUCT_0, ORDERS_2, EQREL_1, RCOMP_1, TOLER_1, ORDERS_3;
definitions TARSKI, XBOOLE_0, PROB_2;
theorems EQREL_1, XBOOLE_0, XBOOLE_1, SUBSET_1, XCMPLX_1, CARD_2, TOLER_1, NAT_1, TARSKI, ZFMISC_1, RELAT_1, RELAT_2, ORDERS_3, CHAIN_1, FUNCT_2, FUNCT_3, RVSUM_1, FINSEQ_1, FINSEQ_3, FUNCT_1, GRFUNC_1, FINSEQ_6, FINSEQ_2, ORDERS_2, SYSREL, FUNCOP_1, ORDERS_1, XREAL_0, ORDINAL1, XXREAL_1, XREAL_1, XXREAL_0;
schemes FUNCT_2, BINOP_2, FINSEQ_2;
registrations XBOOLE_0, SUBSET_1, RELAT_1, PARTFUN1, FINSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, MEMBERED, FINSEQ_1, EQREL_1, STRUCT_0, ORDERS_2, VALUED_0, CARD_1, RELSET_1;
constructors HIDDEN, EQREL_1, PROB_2, RCOMP_1, RVSUM_1, FUNCT_6, REALSET2, ORDERS_3, RELSET_1, BINOP_2, NUMBERS;
requirements HIDDEN, BOOLE, SUBSET, NUMERALS, REAL;
equalities FINSEQ_2, SUBSET_1, CARD_3, STRUCT_0, ORDINAL1;
expansions TARSKI, XBOOLE_0, PROB_2;
Lm1:
for A being RelStr st A is reflexive & A is trivial holds
A is discrete
Lm2:
for A being RelStr st A is discrete holds
A is diagonal
by ORDERS_3:def 1;