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