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

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