let X be set ; :: thesis: for i being Integer
for KX being SimplicialComplexStr of X st KX is subset-closed & degree KX <= i holds
Skeleton_of KX,i = TopStruct(# the carrier of KX,the topology of KX #)
let i be Integer; :: thesis: for KX being SimplicialComplexStr of X st KX is subset-closed & degree KX <= i holds
Skeleton_of KX,i = TopStruct(# the carrier of KX,the topology of KX #)
let KX be SimplicialComplexStr of X; :: thesis: ( KX is subset-closed & degree KX <= i implies Skeleton_of KX,i = TopStruct(# the carrier of KX,the topology of KX #) )
assume that
A1: KX is subset-closed and
A2: degree KX <= i ; :: thesis: Skeleton_of KX,i = TopStruct(# the carrier of KX,the topology of KX #)
set S = Skeleton_of KX,i;
i in REAL by XREAL_0:def 1;
then degree KX < +infty by A2, XXREAL_0:2, XXREAL_0:9;
then A3: ( KX is finite-degree or KX is empty-membered ) by Def12;
then A4: the_family_of KX is finite-membered by MATROID0:def 6;
A5: the topology of KX c= the topology of (Skeleton_of KX,i)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the topology of KX or x in the topology of (Skeleton_of KX,i) )
A6: (degree KX) + 1 <= i + 1 by A2, XXREAL_3:38;
assume A7: x in the topology of KX ; :: thesis: x in the topology of (Skeleton_of KX,i)
then reconsider A = x as finite Subset of KX by A4, MATROID0:def 5;
( A is simplex-like & not KX is void ) by A7, PENCIL_1:def 4, PRE_TOPC:def 5;
then card A <= (degree KX) + 1 by A3, Def12;
then ( card A <= i + 1 & i + 1 in NAT ) by A6, INT_1:16, XXREAL_0:2;
then card (card A) c= card (i + 1) by NAT_1:41;
then A in the_subsets_with_limited_card (i + 1),the topology of KX by A7, Def2;
hence x in the topology of (Skeleton_of KX,i) by Th2; :: thesis: verum

end;

A8: the_subsets_with_limited_card (i + 1),the topology of KX c= the topology of KX

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the_subsets_with_limited_card (i + 1),the topology of KX or x in the topology of KX )
thus ( not x in the_subsets_with_limited_card (i + 1),the topology of KX or x in the topology of KX ) by Def2; :: thesis: verum

end;

the_family_of KX is subset-closed by A1;
then the topology of (Skeleton_of KX,i) c= the topology of KX by A8, Th3;
hence Skeleton_of KX,i = TopStruct(# the carrier of KX,the topology of KX #) by A5, XBOOLE_0:def 10; :: thesis: verum