let S be Subset of K; :: thesis: ( S is empty implies S is simplex-like )
assume A1: S is empty ; :: thesis: S is simplex-like
the topology of K is with_empty_element by Def8;
then S in the topology of K by A1;
hence S is simplex-like ; :: thesis: verum