environ
vocabularies HIDDEN, NUMBERS, FINSEQ_1, ORDINAL4, XBOOLE_0, SUBSET_1, ARYTM_3, RELAT_1, XXREAL_0, CARD_1, NAT_1, FUNCT_1, FINSEQ_5, ARYTM_1, TARSKI, WELLORD1, PBOOLE, RELAT_2, FUNCOP_1, EQREL_1, REWRITE1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, FUNCT_1, RELAT_1, RELAT_2, WELLORD1, EQREL_1, FINSEQ_1, FUNCOP_1, PBOOLE, FINSEQ_5;
definitions TARSKI, RELAT_1, RELAT_2, WELLORD1;
theorems TARSKI, NAT_1, WELLORD1, RELAT_1, RELAT_2, FUNCT_1, FUNCOP_1, FINSEQ_1, FINSEQ_5, EQREL_1, WELLORD2, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, ORDINAL1, CARD_1, PARTFUN1, XTUPLE_0;
schemes NAT_1, RELAT_1, EQREL_1, TREES_2;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, PARTFUN1, NAT_1, XXREAL_0, XREAL_0, FINSEQ_1, CARD_1;
constructors HIDDEN, SETFAM_1, WELLORD1, XXREAL_0, XREAL_0, NAT_1, EQREL_1, PBOOLE, FINSEQ_5, RELSET_1, NUMBERS;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities RELAT_1;
expansions TARSKI, RELAT_2, WELLORD1;
Lm5:
for R being Relation
for a, b being object st a,b are_convertible_wrt R holds
b,a are_convertible_wrt R
definition
let R,
Q be
Relation;
symmetry
for R, Q being Relation st ( for a, b, c being object st [a,b] in R & [a,c] in Q holds
ex d being object st
( Q reduces b,d & R reduces c,d ) ) holds
for a, b, c being object st [a,b] in Q & [a,c] in R holds
ex d being object st
( R reduces b,d & Q reduces c,d )
symmetry
for R, Q being Relation st ( for a, b, c being object st R reduces a,b & Q reduces a,c holds
ex d being object st
( Q reduces b,d & R reduces c,d ) ) holds
for a, b, c being object st Q reduces a,b & R reduces a,c holds
ex d being object st
( R reduces b,d & Q reduces c,d )
end;