theorem :: CLASSES4:85

for UN being Universe holds { u where u is Element of UN : verum } is not Element of UN