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