{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 #);

( 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}:] )
;

verum