let X be set ; :: thesis: ( X is 1 -element implies ( X is trivial & not X is empty ) )
assume X is 1 -element ; :: thesis: ( X is trivial & not X is empty )
then card X = 1
.= card {0} by Th29 ;
then ex x being object st X = {x} by Th4, Th27;
hence ( X is trivial & not X is empty ) ; :: thesis: verum