take
{}
(
bool
the
carrier
of
V
)
;
:: thesis:
(
{}
(
bool
the
carrier
of
V
)
is
empty
&
{}
(
bool
the
carrier
of
V
)
is
affinely-independent
)
thus
(
{}
(
bool
the
carrier
of
V
)
is
empty
&
{}
(
bool
the
carrier
of
V
)
is
affinely-independent
) ;
:: thesis:
verum