theorem Th29: :: LATTICE5:29

for A being non empty set
for O1, O2 being Ordinal st O1 c= O2 holds
ConsecutiveSet (A,O1) c= ConsecutiveSet (A,O2)