a is_associated_to a ;
hence not Class a is empty by Def5; :: thesis: verum