set
x
= the
Element
of
T
;
reconsider
A
=
{
the
Element
of
T
}
as
Subset
of
T
;
Cl
A
=
the
carrier
of
T
by
TEX_1:9
;
hence
ex
b
_{1}
being
Subset
of
T
st
b
_{1}
is
2nd_class
;
:: thesis:
verum