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;