theorem Th17: :: LATTICE8:17

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