dom (R | X) c= X by RELAT_1:58;
hence for b₁ being Relation st b₁ = R | X holds
b₁ is X -defined by RELAT_1:def 18; :: thesis: verum