reconsider
A
=
{}
as
Element
of
S
by
PROB_1:4
;
take
A
;
:: thesis:
M
.
A
=
0.
thus
M
.
A
=
0.
by
VALUED_0:def 19
;
:: thesis:
verum