rng e = (rng e) /\ X ;
hence for b₁ being Relation st b₁ = e null X holds
b₁ is X -valued by RELAT_1:def 19; :: thesis: verum