set C = {0,1};
set R = Total {0,1};
set E = RelStr(# {0,1},(Total {0,1}) #);
reconsider E = RelStr(# {0,1},(Total {0,1}) #) as non empty RelStr ;
( E is with_equivalence & not {0,1} is trivial ) by CHAIN_1:3;
hence ex b₁ being RelStr st
( not b₁ is diagonal & b₁ is finite & b₁ is with_equivalence & not b₁ is empty ) ; :: thesis: verum