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