let S be SubSimplicialComplex of K; :: thesis: S is simplex-join-closed
A1: the topology of S c= the topology of K by SIMPLEX0:def 13;
let A, B be Subset of S; :: according to SIMPLEX1:def 8 :: thesis: ( A is simplex-like & B is simplex-like implies (conv (@ A)) /\ (conv (@ B)) = conv (@ (A /\ B)) )
assume that
A2: A is simplex-like and
A3: B is simplex-like ; :: thesis: (conv (@ A)) /\ (conv (@ B)) = conv (@ (A /\ B))
A4: A in the topology of S by A2;
then A5: A in the topology of K by A1;
A6: B in the topology of S by A3;
then B in the topology of K by A1;
then reconsider A1 = A, B1 = B as Subset of K by A5;
A7: A1 is simplex-like by A1, A4;
B1 is simplex-like by A1, A6;
then (conv (@ A1)) /\ (conv (@ B1)) = conv (@ (A1 /\ B1)) by A7, Def8;
hence (conv (@ A)) /\ (conv (@ B)) = conv (@ (A /\ B)) ; :: thesis: verum