take [#] L ; :: thesis: ( [#] L is meet-closed & [#] L is join-closed & not [#] L is empty )
thus ( [#] L is meet-closed & [#] L is join-closed & not [#] L is empty ) ; :: thesis: verum