let X be set ; 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; 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 ; ( - 1 <= i1 & i1 <= i2 implies Skeleton_of (KX,i1) is SubSimplicialComplex of Skeleton_of (KX,i2) )
assume that
- 1 <= i1
and
A1:
i1 <= i2
; 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)
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; verum