let R be Relation; :: thesis: ( R is real-valued implies R is complex-valued )
assume rng R c= REAL ; :: according to VALUED_0:def 3 :: thesis: R is complex-valued
hence rng R c= COMPLEX by NUMBERS:11; :: according to VALUED_0:def 1 :: thesis: verum