take {0 ,1} ; :: thesis: ( not {0 ,1} is trivial & not {0 ,1} is empty )
for x being set holds not {0 ,1} = {x} by ZFMISC_1:9;
hence ( not {0 ,1} is trivial & not {0 ,1} is empty ) by Def4; :: thesis: verum