environ
vocabularies HIDDEN, FUNCT_1, RELAT_1, FUNCOP_1, NAT_1, TARSKI, ARYTM_3, XBOOLE_0, SUBSET_1, NUMBERS, XXREAL_0, FINSET_1, CARD_1, ORDERS_2, REARRAN1, RELAT_2, STRUCT_0, WELLORD1, WAYBEL_4, WAYBEL20, EQREL_1, ORDERS_1, ZFMISC_1, WELLFND1, SETFAM_1, VALUED_0, ORDINAL2, MCART_1, CAT_1, YELLOW_1, PBOOLE, CARD_3, RLVECT_2, YELLOW_6, WAYBEL_3, FUNCT_4, YELLOW_3, DICKSON, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, PBOOLE, RELSET_1, XXREAL_2, SEQ_4, PARTFUN1, FUNCT_2, CARD_3, ORDINAL1, XCMPLX_0, NAT_1, STRUCT_0, RELAT_2, XXREAL_0, FUNCT_4, FUNCOP_1, DOMAIN_1, FINSET_1, XTUPLE_0, MCART_1, WELLORD1, ORDERS_2, ORDERS_1, EQREL_1, WELLFND1, WAYBEL_0, CARD_1, NUMBERS, WAYBEL_4, VALUED_0, PRALG_1, YELLOW_3, WAYBEL_1, YELLOW_1, WAYBEL_3, YELLOW_6;
definitions TARSKI, RELAT_2, ORDERS_2, ORDERS_1;
theorems WELLORD1, ORDERS_1, SUBSET_1, TARSKI, RELAT_1, RELAT_2, RELSET_1, ZFMISC_1, EQREL_1, WAYBEL_0, ORDERS_2, NAT_1, FUNCT_1, FUNCT_2, CARD_2, CARD_1, NORMSP_1, SEQM_3, FINSET_1, AXIOMS, YELLOW_3, WAYBEL_1, WAYBEL20, YELLOW_1, CARD_3, FUNCOP_1, WAYBEL_3, MCART_1, FUNCT_4, WELLFND1, WAYBEL_4, PRALG_1, YELLOW_6, AFINSQ_1, XBOOLE_0, XBOOLE_1, PARTFUN1, XXREAL_0, ORDINAL1, XXREAL_2, VALUED_0, XTUPLE_0, NUMBERS;
schemes PRE_CIRC, RECDEF_1, NAT_1, FUNCT_2, DOMAIN_1, FRAENKEL, FINSEQ_1, FUNCT_1, RELSET_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1, FINSET_1, XXREAL_0, NAT_1, MEMBERED, EQREL_1, PRE_CIRC, STRUCT_0, ORDERS_2, YELLOW_1, YELLOW_3, WAYBEL18, WAYBEL_3, VALUED_0, CARD_1, XXREAL_2, CARD_3, ZFMISC_1, RELSET_1, XTUPLE_0, XCMPLX_0;
constructors HIDDEN, WELLORD1, DOMAIN_1, PRALG_1, ORDERS_3, WAYBEL_1, YELLOW_3, WAYBEL_3, WAYBEL_4, WELLFND1, SEQ_4, RELSET_1, XTUPLE_0, NUMBERS;
requirements HIDDEN, BOOLE, SUBSET, NUMERALS;
equalities FUNCOP_1, ORDINAL1, CARD_1;
expansions TARSKI, RELAT_2, ORDERS_2, ORDERS_1;
definition
let R be
RelStr ;
existence
ex b1 being Relation of (Class (EqRel R)) st
for A, B being object holds
( [A,B] in b1 iff ex a, b being Element of R st
( A = Class ((EqRel R),a) & B = Class ((EqRel R),b) & a <= b ) )
uniqueness
for b1, b2 being Relation of (Class (EqRel R)) st ( for A, B being object holds
( [A,B] in b1 iff ex a, b being Element of R st
( A = Class ((EqRel R),a) & B = Class ((EqRel R),b) & a <= b ) ) ) & ( for A, B being object holds
( [A,B] in b2 iff ex a, b being Element of R st
( A = Class ((EqRel R),a) & B = Class ((EqRel R),b) & a <= b ) ) ) holds
b1 = b2
end;
Lm1:
for p being RelStr-yielding ManySortedSet of {} holds
( not product p is empty & product p is quasi_ordered & product p is Dickson & product p is antisymmetric )