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