(
rng
R
c=
Y
&
dom
(
R
~
)
=
rng
R
)
by
RELAT_1:20
;
hence
for
b
_{1}
being
Relation
st
b
_{1}
=
R
~
holds
b
_{1}
is
Y
-defined
by
RELAT_1:def 18
;
:: thesis:
verum