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

( 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