let T be TopSpace; :: thesis: {} T is perfect
Der ({} T) = {} T by Th42;
hence {} T is perfect by Th43; :: thesis: verum