consider A being non empty trivial finite reflexive transitive antisymmetric RelStr ;
A is Chain by Def1;
hence ex b₁ being Chain st
( b₁ is finite & not b₁ is empty ) ; :: thesis: verum