environ
vocabularies HIDDEN, XBOOLE_0, RELAT_2, RELAT_1, EQREL_1, WELLORD1, ZFMISC_1, PARTFUN1, SUBSET_1, TARSKI, ORDINAL1, TOLER_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELSET_1, RELAT_2, PARTFUN1, ORDINAL1, WELLORD1, EQREL_1;
definitions TARSKI, RELAT_1, RELAT_2;
theorems TARSKI, RELAT_1, RELSET_1, RELAT_2, ZFMISC_1, WELLORD1, ENUMSET1, ORDERS_1, EQREL_1, ORDINAL1, XBOOLE_0, XBOOLE_1, PARTFUN1, XTUPLE_0;
schemes XBOOLE_0, XFAMILY;
registrations XBOOLE_0, SUBSET_1, RELAT_1, PARTFUN1, EQREL_1, RELSET_1;
constructors HIDDEN, ORDINAL1, WELLORD1, EQREL_1, RELSET_1;
requirements HIDDEN, SUBSET, BOOLE;
equalities RELAT_1, WELLORD1;
expansions TARSKI, RELAT_1, RELAT_2;
scheme
ToleranceEx{
F1()
-> set ,
P1[
object ,
object ] } :
ex
T being
Tolerance of
F1() st
for
x,
y being
set st
x in F1() &
y in F1() holds
(
[x,y] in T iff
P1[
x,
y] )
provided
A1:
for
x being
set st
x in F1() holds
P1[
x,
x]
and A2:
for
x,
y being
set st
x in F1() &
y in F1() &
P1[
x,
y] holds
P1[
y,
x]