let D be set ; :: thesis: {} in D *
{} = <*> D ;
hence {} in D * by Def11; :: thesis: verum