let T be TopStruct ; :: thesis: {} is empty compact Subset of T
{} T c= the carrier of T ;
hence {} is empty compact Subset of T ; :: thesis: verum