R .: X c= rng R by RELAT_1:111;
hence R .: X is integer-membered ; :: thesis: verum