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 by Def13
.= card {0} by Th50 ;
then ex x being set st X = {x} by Th49;
hence ( X is trivial & not X is empty ) ; :: thesis: verum