take [#] L ; :: thesis: ( [#] L is initial & [#] L is final & not [#] L is empty )
thus ( [#] L is initial & [#] L is final & not [#] L is empty ) ; :: thesis: verum