let A be non empty Poset; :: thesis: for S being Subset of A st the InternalRel of A linearly_orders S holds
S is Chain of A
let S be Subset of A; :: thesis: ( the InternalRel of A linearly_orders S implies S is Chain of A )
assume the InternalRel of A linearly_orders S ; :: thesis: S is Chain of A
then ( the InternalRel of A is_reflexive_in S & the InternalRel of A is_connected_in S ) by ORDERS_1:def 8;
then the InternalRel of A is_strongly_connected_in S by ORDERS_1:92;
hence S is Chain of A by Def11; :: thesis: verum