theorem Th30: :: ENS_1:31

for V being non empty set
for a being Object of (Ens V) st {} in V & a is initial holds
a = {}