take IntRel L ; :: thesis: IntRel L is auxiliary(i)
thus IntRel L is auxiliary(i) ; :: thesis: verum