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