let R be Relation; :: thesis: for S being ext-real-valued Relation st R c= S holds
R is ext-real-valued
let S be ext-real-valued Relation; :: thesis: ( R c= S implies R is ext-real-valued )
assume R c= S ; :: thesis: R is ext-real-valued
then A1: rng R c= rng S by RELAT_1:25;
rng S c= ExtREAL by Def2;
hence rng R c= ExtREAL by A1, XBOOLE_1:1; :: according to VALUED_0:def 2 :: thesis: verum