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