for R being 1-sorted
for X, Y being Subset of R holds
( X c= Y iff (X `) \/ Y = [#] R )