theorem
Th30
:
:: MONOID_1:30
for
X
,
Y
being
set
holds
chi
(
Y
,
X
) is
Multiset
of
X