defpred S₁[ set ] means ex S being c=-linear finite simplex-like Subset-Family of KX st $1 = P .: S;
set SS = { A where A is Subset of KX : S₁[A] } ;
{ A where A is Subset of KX : S₁[A] } c= bool the carrier of KX

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { A where A is Subset of KX : S₁[A] } or x in bool the carrier of KX )
assume x in { A where A is Subset of KX : S₁[A] } ; :: thesis: x in bool the carrier of KX
then ex A being Subset of KX st
( x = A & S₁[A] ) ;
hence x in bool the carrier of KX ; :: thesis: verum

end;

then reconsider SS = { A where A is Subset of KX : S₁[A] } as Subset-Family of KX ;
set PP = TopStruct(# the carrier of KX,SS #);
( [#] TopStruct(# the carrier of KX,SS #) = [#] KX & [#] KX c= X ) by Def9;
then reconsider PP = TopStruct(# the carrier of KX,SS #) as strict SimplicialComplexStr of X by Def9;
take PP ; :: thesis: ( [#] PP = [#] KX & ( for A being Subset of PP holds
( A is simplex-like iff ex S being c=-linear finite simplex-like Subset-Family of KX st A = P .: S ) ) )
thus [#] PP = [#] KX ; :: thesis: for A being Subset of PP holds
( A is simplex-like iff ex S being c=-linear finite simplex-like Subset-Family of KX st A = P .: S )
let A be Subset of PP; :: thesis: ( A is simplex-like iff ex S being c=-linear finite simplex-like Subset-Family of KX st A = P .: S )

hereby :: thesis: ( ex S being c=-linear finite simplex-like Subset-Family of KX st A = P .: S implies A is simplex-like )

assume A is simplex-like ; :: thesis: S₁[A]
then A in SS ;
then ex B being Subset of KX st
( B = A & S₁[B] ) ;
hence S₁[A] ; :: thesis: verum

end;

assume S₁[A] ; :: thesis: A is simplex-like
then A in SS ;
hence A is simplex-like ; :: thesis: verum