theorem Th22: :: LATTICE5:22

for A being non empty set
for O being Ordinal holds ConsecutiveSet (A,(succ O)) = new_set (ConsecutiveSet (A,O))