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