theorem :: ORDINAL4:36
for W being Universe
for phi being Ordinal-Sequence of W st phi is increasing & phi is continuous & omega in W holds
ex A being Ordinal st
( A in dom phi & phi . A = A )