{0} c= {0,1,2} by SETWISEO:1;
then reconsider r = [:{0},{0,1,2}:] as Relation of {0,1,2} by ZFMISC_1:96;
take X = ARS(# {0,1,2},r #); :: thesis: ( the carrier of X = {0,1,2} & the reduction of X = [:{0},{0,1,2}:] )
thus ( the carrier of X = {0,1,2} & the reduction of X = [:{0},{0,1,2}:] ) ; :: thesis: verum