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