set C = Complex_of Y;
reconsider Y1 = Y as Subset-Family of (union Y) by ZFMISC_1:82;
subset-closed_closure_of Y1 c= bool (union Y) ;
then A1: union the topology of (Complex_of Y) c= union (bool (union Y)) by ZFMISC_1:77;
union (bool (union Y)) = union Y by ZFMISC_1:81;
then Vertices (Complex_of Y) c= union Y by A1, Lm5;
hence Complex_of Y is finite-vertices ; :: thesis: verum