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