for A being Ordinal
for X being set st A in X holds
inf X in X