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