theorem Th24: :: LATTICE5:24

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