let X be set ; :: thesis: ( X is trivial & not X is empty implies X is 1 -element )
assume ( X is trivial & not X is empty ) ; :: thesis: X is 1 -element
then ex x being object st X = {x} by ZFMISC_1:131;
hence X is 1 -element ; :: thesis: verum