reconsider E = {} as Relation of 1 by RELSET_1:12;
set X = RelStr(# 1,E #);
reconsider X = RelStr(# 1,E #) as non empty RelStr ;
X is void ;
hence ex b₁ being RelStr st
( not b₁ is empty & b₁ is void ) ; :: thesis: verum