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