{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

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