let K be SimplicialComplexStr of RLS; :: thesis: ( K is empty-membered implies K is simplex-join-closed )
assume K is empty-membered ; :: thesis: K is simplex-join-closed
then A1: the topology of K is empty-membered ;
let A, B be Subset of K; :: 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))
A in the topology of K by A2;
then A4: A is empty by A1;
B in the topology of K by A3;
then B is empty by A1;
hence (conv (@ A)) /\ (conv (@ B)) = conv (@ (A /\ B)) by A4; :: thesis: verum