take {} ; :: thesis: ( {} is relation of X & {} is relation_length of k )
thus ( {} is relation of X & {} is relation_length of k ) by Th4, Th5; :: thesis: verum