theorem Th11: :: WELLORD2:17

for X being set ex R being Relation st R well_orders X