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