theorem Th29: :: FOMODEL0:29

for Y, X being set holds
( ( X \+\ Y = {} implies X = Y ) & ( X = Y implies X \+\ Y = {} ) & ( X \ Y = {} implies X c= Y ) & ( X c= Y implies X \ Y = {} ) & ( for x being object holds
( {x} \ Y = {} iff x in Y ) ) )