let T be TopSpace; :: thesis: Der ({} T) = {} T
Cl ({} T) is empty ;
then {} = ({} T) \/ (Der ({} T)) by Th29
.= Der ({} T) ;
hence Der ({} T) = {} T ; :: thesis: verum