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 by SIMPLEX0:def 7;
let A, B be Subset of K; :: according to SIMPLEX1:def 8 :: thesis: ( not A is dependent & not B is dependent implies (conv (@ A)) /\ (conv (@ B)) = conv (@ (A /\ B)) )
assume that
A2: not A is dependent and
A3: not B is dependent ; :: thesis: (conv (@ A)) /\ (conv (@ B)) = conv (@ (A /\ B))
A in the topology of K by A2, PRE_TOPC:def 5;
then A4: A is empty by A1, SETFAM_1:def 11;
B in the topology of K by A3, PRE_TOPC:def 5;
then B is empty by A1, SETFAM_1:def 11;
hence (conv (@ A)) /\ (conv (@ B)) = conv (@ (A /\ B)) by A4; :: thesis: verum