theorem :: CLASSES5:103

for U being Universe holds [:U,U:] \ [:(U \ {{}}),{{}}:] is not Element of U