(dom R) null X c= (dom R) \/ X ;
hence for b₁ being Relation st b₁ = R null X holds
b₁ is X \/ (dom R) -defined ; :: thesis: verum