R
.:
A
c=
rng
R
by
RELAT_1:111
;
hence
R
.:
A
is
Subset
of
Y
by
XBOOLE_1:1
;
:: thesis:
verum