let X be set ; :: thesis: for KX being SimplicialComplexStr of X
for i being dim-like number 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: for i being dim-like number 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 dim-like number ; :: 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 object ; :: 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:36;
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;
( A is simplex-like & not KX is void ) by A7, PENCIL_1:def 4;
then card A <= (degree KX) + 1 by A3, Def12;
then ( card A <= i + 1 & i + 1 in NAT ) by A6, INT_1:3, XXREAL_0:2;
then card (Segm (card A)) c= card (Segm (i + 1)) by NAT_1:40;
then A in the_subsets_with_limited_card ((Segm (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 ((Segm (i + 1)), the topology of KX) c= the topology of KX by Def2;
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