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 Def2, CHAIN_1:4;
hence ex b₁ being RelStr st
( not b₁ is diagonal & b₁ is finite & b₁ is with_equivalence & not b₁ is empty ) ; :: thesis: verum