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