let A be Chain ; :: thesis: ( A is reflexive & A is transitive & A is antisymmetric )
( A is non empty connected Poset or A is empty RelStr ) by Def1;
hence ( A is reflexive & A is transitive & A is antisymmetric ) ; :: thesis: verum