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, SETFAM_1:def 9;
hence S is simplex-like by PRE_TOPC:def 5; :: thesis: verum