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