consider A being non empty trivial 1-sorted ;
take A ; :: thesis: ( A is trivial & not A is empty )
thus ( A is trivial & not A is empty ) ; :: thesis: verum