for S being 1-sorted
for X being Subset of S holds
( X ` = the carrier of S iff X is empty )