let X be set ; :: thesis: {} is relation of X
thus for a being FinSequence st a in {} holds
rng a c= X ; :: according to MARGREL1:def 5 :: thesis: verum