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

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