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