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 ;
A1: E is with_equivalence by Def2;
not E is diagonal

proof

not {0 ,1} is trivial by CHAIN_1:4;
hence not E is diagonal ; :: thesis: verum

end;

hence ex b₁ being RelStr st
( not b₁ is diagonal & b₁ is finite & b₁ is with_equivalence & not b₁ is empty ) by A1; :: thesis: verum