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

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