X c= tau X by Th16;
hence not tau X is empty ; :: thesis: verum