let
X
be
set
;
:: thesis:
for
b
being
bag
of
X
holds
b
/
b
=
EmptyBag
X
let
b
be
bag
of
X
;
:: thesis:
b
/
b
=
EmptyBag
X
b
+
(
EmptyBag
X
)
=
b
by
PRE_POLY:53
;
hence
b
/
b
=
EmptyBag
X
by
Def1
;
:: thesis:
verum