for X, Y being set holds
( X \ Y = {} iff X c= Y ) by Lm1;