take [#] V ; :: thesis: ( [#] V is add-closed & [#] V is having-inverse & not [#] V is empty )
thus ( [#] V is add-closed & [#] V is having-inverse & not [#] V is empty ) ; :: thesis: verum