the
carrier
of
S
in
{
the
carrier
of
S
}
by
TARSKI:def 1
;
then
[
o
, the
carrier
of
S
]
in
[:
the
carrier'
of
S
,
{
the
carrier
of
S
}
:]
by
ZFMISC_1:87
;
then
[
o
, the
carrier
of
S
]
in
NonTerminals
(
DTConMSA
X
)
by
Th6
;
hence
[
o
, the
carrier
of
S
]
is
Symbol
of
(
DTConMSA
X
)
;
:: thesis:
verum