theorem Th13: :: ORDERS_2:13

for A being RelStr
for T being Subset of A st the InternalRel of A well_orders T holds
T is Chain of A by ORDERS_1:7, Def7;