set E = RelStr(# {{}},(id {{}}) #);
RelStr(# {{}},(id {{}}) #) is discrete ;
hence ex b₁ being RelStr st
( b₁ is discrete & b₁ is finite & b₁ is with_equivalence & not b₁ is empty ) ; :: thesis: verum