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