IntRel L is auxiliary Relation of ;
hence not Aux L is empty by Def9; :: thesis: verum