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: ( 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))
A4: A in the topology of S by A2, PRE_TOPC:def 2;
then A5: A in the topology of K by A1;
A6: B in the topology of S by A3, PRE_TOPC:def 2;
then B in the topology of K by A1;
then reconsider A1 = A, B1 = B as Subset of K by A5;
A7: not A1 is dependent by A1, A4, PRE_TOPC:def 2;
not B1 is dependent by A1, A6, PRE_TOPC:def 2;
then (conv (@ A1)) /\ (conv (@ B1)) = conv (@ (A1 /\ B1)) by A7, Def8;
hence (conv (@ A)) /\ (conv (@ B)) = conv (@ (A /\ B)) ; :: thesis: verum