[:a,b:] is Relation of a,b by RELSET_1:def 1;
hence not for b₁ being Relation of a,b holds b₁ is empty ; :: thesis: verum