let X be set ; :: thesis: for KX being SimplicialComplexStr of X
for i1, i2 being dim-like number st - 1 <= i1 & i1 <= i2 holds
Skeleton_of (KX,i1) is SubSimplicialComplex of Skeleton_of (KX,i2)
let KX be SimplicialComplexStr of X; :: thesis: for i1, i2 being dim-like number st - 1 <= i1 & i1 <= i2 holds
Skeleton_of (KX,i1) is SubSimplicialComplex of Skeleton_of (KX,i2)
let i1, i2 be dim-like number ; :: thesis: ( - 1 <= i1 & i1 <= i2 implies Skeleton_of (KX,i1) is SubSimplicialComplex of Skeleton_of (KX,i2) )
assume that
- 1 <= i1 and
A1: i1 <= i2 ; :: thesis: Skeleton_of (KX,i1) is SubSimplicialComplex of Skeleton_of (KX,i2)
reconsider I1 = i1 + 1, I2 = i2 + 1 as Element of NAT by INT_1:3;
the_subsets_with_limited_card ((Segm (i1 + 1)), the topology of KX) c= the_subsets_with_limited_card ((Segm (i2 + 1)), the topology of KX)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the_subsets_with_limited_card ((Segm (i1 + 1)), the topology of KX) or x in the_subsets_with_limited_card ((Segm (i2 + 1)), the topology of KX) )
reconsider xx = x as set by TARSKI:1;
I1 <= I2 by A1, XREAL_1:6;
then A2: card (Segm I1) c= card (Segm I2) by NAT_1:40;
assume A3: x in the_subsets_with_limited_card ((Segm (i1 + 1)), the topology of KX) ; :: thesis: x in the_subsets_with_limited_card ((Segm (i2 + 1)), the topology of KX)
then card xx c= card I1 by Def2;
then A4: card xx c= card I2 by A2;
x in the topology of KX by A3, Def2;
hence x in the_subsets_with_limited_card ((Segm (i2 + 1)), the topology of KX) by A4, Def2; :: thesis: verum

end;

then the_subsets_with_limited_card ((Segm (i1 + 1)), the topology of KX) is_finer_than the_subsets_with_limited_card ((Segm (i2 + 1)), the topology of KX) ;
then A5: the topology of (Skeleton_of (KX,i1)) c= the topology of (Skeleton_of (KX,i2)) by Th6;
[#] (Skeleton_of (KX,i1)) = [#] (Skeleton_of (KX,i2)) ;
hence Skeleton_of (KX,i1) is SubSimplicialComplex of Skeleton_of (KX,i2) by A5, Def13; :: thesis: verum