let X be set ; :: thesis: for Y1, Y2 being Subset-Family of X st Y1 is finite-membered & Y1 is_finer_than Y2 holds
Complex_of Y1 is SubSimplicialComplex of Complex_of Y2
let Y1, Y2 be Subset-Family of X; :: thesis: ( Y1 is finite-membered & Y1 is_finer_than Y2 implies Complex_of Y1 is SubSimplicialComplex of Complex_of Y2 )
assume that
A1: Y1 is finite-membered and
A2: Y1 is_finer_than Y2 ; :: thesis: Complex_of Y1 is SubSimplicialComplex of Complex_of Y2
set C1 = Complex_of Y1;
set C2 = Complex_of Y2;
A3: ( [#] (Complex_of Y1) = X & [#] (Complex_of Y2) = X ) ;
subset-closed_closure_of Y1 c= subset-closed_closure_of Y2 by A2, Th6;
hence Complex_of Y1 is SubSimplicialComplex of Complex_of Y2 by A1, A3, Def13; :: thesis: verum