consider A being non empty trivial reflexive transitive antisymmetric RelStr ;
A is Chain by Def1;
hence not for b₁ being Chain holds b₁ is empty ; :: thesis: verum