Coim R,x = R " {x} ;
hence Coim R,x is Subset of X ; :: thesis: verum