theorem :: ORDINAL6:31

for x being set
for f being Ordinal-Sequence st x in dom (criticals f) holds
x c= (criticals f) . x by ORDINAL4:10;