R
"
A
c=
dom
R
by
RELAT_1:132
;
hence
R
"
A
is
Subset
of
X
by
XBOOLE_1:1
;
:: thesis:
verum