let X be set ; for KX being SimplicialComplexStr of X
for K1, K2 being maximal SubSimplicialComplex of KX st [#] K1 = [#] K2 holds
TopStruct(# the carrier of K1, the topology of K1 #) = TopStruct(# the carrier of K2, the topology of K2 #)
let KX be SimplicialComplexStr of X; for K1, K2 being maximal SubSimplicialComplex of KX st [#] K1 = [#] K2 holds
TopStruct(# the carrier of K1, the topology of K1 #) = TopStruct(# the carrier of K2, the topology of K2 #)
let K1, K2 be maximal SubSimplicialComplex of KX; ( [#] K1 = [#] K2 implies TopStruct(# the carrier of K1, the topology of K1 #) = TopStruct(# the carrier of K2, the topology of K2 #) )
assume A1:
[#] K1 = [#] K2
; TopStruct(# the carrier of K1, the topology of K1 #) = TopStruct(# the carrier of K2, the topology of K2 #)
set TOP1 = the topology of K1;
set TOP2 = the topology of K2;
set TOP = the topology of KX;
A2:
the topology of KX /\ (bool ([#] K2)) c= the topology of K2
by Th33;
the topology of K1 c= the topology of KX
by Def13;
then A3:
the topology of K1 c= the topology of KX /\ (bool ([#] K1))
by XBOOLE_1:19;
the topology of K2 c= the topology of KX
by Def13;
then A4:
the topology of K2 c= the topology of KX /\ (bool ([#] K2))
by XBOOLE_1:19;
the topology of KX /\ (bool ([#] K1)) c= the topology of K1
by Th33;
then the topology of K1 =
the topology of KX /\ (bool ([#] K1))
by A3
.=
the topology of K2
by A1, A2, A4
;
hence
TopStruct(# the carrier of K1, the topology of K1 #) = TopStruct(# the carrier of K2, the topology of K2 #)
by A1; verum