take {{}} ; :: thesis: ( {{}} is finite-membered & not {{}} is empty )
thus ( {{}} is finite-membered & not {{}} is empty ) ; :: thesis: verum