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