take {{} } ; :: thesis: ( not {{} } is empty & {{} } is functional )
thus ( not {{} } is empty & {{} } is functional ) ; :: thesis: verum