let T be TopSpace; :: thesis: Der ({} T) = {} T

per cases ( not T is empty or T is empty ) ;

suppose not T is empty ; :: thesis: Der ({} T) = {} T

then reconsider T' = T as non empty TopSpace ;
Cl ({} T') is empty ;
then {} = ({} T) \/ (Der ({} T)) by Th31
.= Der ({} T) ;
hence Der ({} T) = {} T ; :: thesis: verum

end;

suppose T is empty ; :: thesis: Der ({} T) = {} T

hence Der ({} T) = {} T by Lm1; :: thesis: verum

end;

end;