for W being Universe
for a being Ordinal of W holds not On W is_cofinal_with a