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