reconsider C = Complex_of the topology of K as SubdivisionStr of K by Th12;
reconsider SF = Sub_of_Fin the topology of C as Subset-Family of C by XBOOLE_1:1;
Complex_of SF is SubdivisionStr of C by Th13;
then reconsider CSF = Complex_of SF as SubdivisionStr of K by Th14;
take CSF ; :: thesis: ( CSF is finite-membered & CSF is subset-closed )
thus ( CSF is finite-membered & CSF is subset-closed ) ; :: thesis: verum