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