let A be non empty Poset; :: thesis: for C being Chain of A holds the InternalRel of A linearly_orders C
let C be Chain of A; :: thesis: the InternalRel of A linearly_orders C
A1: the InternalRel of A is_antisymmetric_in the carrier of A by Def6;
( the InternalRel of A is_reflexive_in the carrier of A & the InternalRel of A is_transitive_in the carrier of A ) by Def4, Def5;
hence ( the InternalRel of A is_reflexive_in C & the InternalRel of A is_transitive_in C & the InternalRel of A is_antisymmetric_in C ) by A1, ORDERS_1:8, ORDERS_1:9, ORDERS_1:10; :: according to ORDERS_1:def 8 :: thesis: the InternalRel of A is_connected_in C
the InternalRel of A is_strongly_connected_in C by Def11;
hence the InternalRel of A is_connected_in C by ORDERS_1:7; :: thesis: verum