let A be RelStr ; :: thesis: for T being Subset of A st the InternalRel of A well_orders T holds
T is Chain of A
let T be Subset of A; :: thesis: ( the InternalRel of A well_orders T implies T is Chain of A )
assume the InternalRel of A well_orders T ; :: thesis: T is Chain of A
then ( the InternalRel of A is_connected_in T & the InternalRel of A is_reflexive_in T ) by WELLORD1:def 5;
then the InternalRel of A is_strongly_connected_in T by ORDERS_1:7;
hence T is Chain of A by Def11; :: thesis: verum