let k be Element of NAT ; :: thesis: {} is relation_length of k
thus for a being FinSequence st a in {} holds
len a = k ; :: according to MARGREL1:def 4 :: thesis: verum