theorem :: ORDINAL6:48

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