let X, Y be set ; :: thesis: ( {} is X -defined & {} is Y -valued )
thus ( dom {} c= X & rng {} c= Y ) ; :: according to RELAT_1:def 18,RELAT_1:def 19 :: thesis: verum