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