let K be SimplicialComplexStr; :: thesis: for S being Subset-Family of K holds
( S is simplex-like iff S c= the topology of K )
let S be Subset-Family of K; :: thesis: ( S is simplex-like iff S c= the topology of K )

hereby :: thesis: ( S c= the topology of K implies S is simplex-like )

assume A1: S is simplex-like ; :: thesis: S c= the topology of K
thus S c= the topology of K :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in S or x in the topology of K )
assume A2: x in S ; :: thesis: x in the topology of K
then reconsider A = x as Subset of K ;
A is simplex-like by A1, A2;
hence x in the topology of K ; :: thesis: verum

end;

end;

assume A3: S c= the topology of K ; :: thesis: S is simplex-like
let A be Subset of K; :: according to TOPS_2:def 1 :: thesis: ( not A in S or A is simplex-like )
assume A in S ; :: thesis: A is simplex-like
hence A is simplex-like by A3; :: thesis: verum