take
{
the
Element
of
V
}
;
:: thesis:
(
{
the
Element
of
V
}
is 1
-element
&
{
the
Element
of
V
}
is
affinely-independent
)
thus
(
{
the
Element
of
V
}
is 1
-element
&
{
the
Element
of
V
}
is
affinely-independent
) ;
:: thesis:
verum