take IntRel L ; :: thesis: IntRel L is extra-order
thus IntRel L is extra-order ; :: thesis: verum