defpred
S
_{1}
[
object
]
means
ex
R
being
strict
RelStr
st
( $1
=
R
& the
carrier
of
R
in
FinSETS
);
thus
for
X1
,
X2
being
set
st ( for
x
being
object
holds
(
x
in
X1
iff
S
_{1}
[
x
] ) ) & ( for
x
being
object
holds
(
x
in
X2
iff
S
_{1}
[
x
] ) ) holds
X1
=
X2
from
XBOOLE_0:sch 3
();
:: thesis:
verum