let P1, P2 be strict SimplicialComplexStr of X; :: thesis: ( [#] P1 = [#] KX & ( for A being Subset of P1 holds
( A is simplex-like iff ex S being c=-linear finite simplex-like Subset-Family of KX st A = P .: S ) ) & [#] P2 = [#] KX & ( for A being Subset of P2 holds
( A is simplex-like iff ex S being c=-linear finite simplex-like Subset-Family of KX st A = P .: S ) ) implies P1 = P2 )
assume that
A1: [#] P1 = [#] KX and
A2: for A being Subset of P1 holds
( A is simplex-like iff ex S being c=-linear finite simplex-like Subset-Family of KX st A = P .: S ) and
A3: [#] P2 = [#] KX and
A4: for A being Subset of P2 holds
( A is simplex-like iff ex S being c=-linear finite simplex-like Subset-Family of KX st A = P .: S ) ; :: thesis: P1 = P2

now :: thesis: for x being object holds
( ( x in the topology of P1 implies x in the topology of P2 ) & ( x in the topology of P2 implies x in the topology of P1 ) )

let x be object ; :: thesis: ( ( x in the topology of P1 implies x in the topology of P2 ) & ( x in the topology of P2 implies x in the topology of P1 ) )

hereby :: thesis: ( x in the topology of P2 implies x in the topology of P1 )

assume A5: x in the topology of P1 ; :: thesis: x in the topology of P2
then reconsider A = x as Subset of P1 ;
reconsider B = A as Subset of P2 by A1, A3;
A is simplex-like by A5;
then ex S being c=-linear finite simplex-like Subset-Family of KX st A = P .: S by A2;
then B is simplex-like by A4;
hence x in the topology of P2 ; :: thesis: verum

end;

assume A6: x in the topology of P2 ; :: thesis: x in the topology of P1
then reconsider A = x as Subset of P2 ;
reconsider B = A as Subset of P1 by A1, A3;
A is simplex-like by A6;
then ex S being c=-linear finite simplex-like Subset-Family of KX st A = P .: S by A4;
then B is simplex-like by A2;
hence x in the topology of P1 ; :: thesis: verum

end;

hence P1 = P2 by A1, A3, TARSKI:2; :: thesis: verum