theorem Th15: :: LATTICE8:15

for A being non empty set
for O being Ordinal holds ConsecutiveSet2 (A,(succ O)) = new_set2 (ConsecutiveSet2 (A,O))