let X be set ; :: thesis: for i1, i2 being Integer
for KX being SimplicialComplexStr of X st - 1 <= i1 & i1 <= i2 holds
Skeleton_of (KX,i1) is SubSimplicialComplex of Skeleton_of (KX,i2)
let i1, i2 be Integer; :: thesis: for KX being SimplicialComplexStr of X st - 1 <= i1 & i1 <= i2 holds
Skeleton_of (KX,i1) is SubSimplicialComplex of Skeleton_of (KX,i2)
let KX be SimplicialComplexStr of X; :: thesis: ( - 1 <= i1 & i1 <= i2 implies Skeleton_of (KX,i1) is SubSimplicialComplex of Skeleton_of (KX,i2) )
assume that
A1: - 1 <= i1 and
A2: i1 <= i2 ; :: thesis: Skeleton_of (KX,i1) is SubSimplicialComplex of Skeleton_of (KX,i2)
- 1 <= i2 by A1, A2, XXREAL_0:2;
then A3: (- 1) + 1 <= i2 + 1 by XREAL_1:8;
(- 1) + 1 <= i1 + 1 by A1, XREAL_1:8;
then reconsider I1 = i1 + 1, I2 = i2 + 1 as Element of NAT by A3, INT_1:16;
the_subsets_with_limited_card ((i1 + 1), the topology of KX) c= the_subsets_with_limited_card ((i2 + 1), the topology of KX)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the_subsets_with_limited_card ((i1 + 1), the topology of KX) or x in the_subsets_with_limited_card ((i2 + 1), the topology of KX) )
I1 <= I2 by A2, XREAL_1:8;
then A4: card I1 c= card I2 by NAT_1:41;
assume A5: x in the_subsets_with_limited_card ((i1 + 1), the topology of KX) ; :: thesis: x in the_subsets_with_limited_card ((i2 + 1), the topology of KX)
then card x c= card I1 by Def2;
then A6: card x c= card I2 by A4, XBOOLE_1:1;
x in the topology of KX by A5, Def2;
hence x in the_subsets_with_limited_card ((i2 + 1), the topology of KX) by A6, Def2; :: thesis: verum

end;

then the_subsets_with_limited_card ((i1 + 1), the topology of KX) is_finer_than the_subsets_with_limited_card ((i2 + 1), the topology of KX) by SETFAM_1:17;
then A7: 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 A7, Def13; :: thesis: verum