let X be set ; :: thesis: ( Total X c= id X implies X is trivial )
assume A1: Total X c= id X ; :: thesis: X is trivial
assume not X is trivial ; :: thesis: contradiction
then consider x, y being object such that
A2: ( x in X & y in X ) and
A3: x <> y by ZFMISC_1:def 10;
[x,y] in Total X by A2, TOLER_1:2;
hence contradiction by A1, A3, RELAT_1:def 10; :: thesis: verum