take
{
the
Element
of
T
}
;
:: thesis:
( not
{
the
Element
of
T
}
is
empty
&
{
the
Element
of
T
}
is
compact
&
{
the
Element
of
T
}
is
connected
)
thus
( not
{
the
Element
of
T
}
is
empty
&
{
the
Element
of
T
}
is
compact
&
{
the
Element
of
T
}
is
connected
) ;
:: thesis:
verum