for W being Universe
for a being Object of (Ens W) st a is initial holds
a = {} by Th30, CLASSES2:56;