let D be set ; :: thesis: {} in D ^omega
{} = <%> D ;
hence {} in D ^omega by Def8; :: thesis: verum