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 Def4;
( the InternalRel of A is_reflexive_in the carrier of A & the InternalRel of A is_transitive_in the carrier of A ) by Def2, Def3;
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; :: according to ORDERS_1:def 9 :: thesis: the InternalRel of A is_connected_in C
the InternalRel of A is_strongly_connected_in C by Def7;
hence the InternalRel of A is_connected_in C ; :: thesis: verum