theorem Th9: :: ZF_REFLE:9

for L being Ordinal-Sequence
for A being Ordinal holds L | (Rank A) is Ordinal-Sequence