let V be RealLinearSpace; :: thesis: for K being subset-closed SimplicialComplexStr of V holds
( K is simplex-join-closed iff for A, B being Subset of K st A is simplex-like & B is simplex-like & Int (@ A) meets Int (@ B) holds
A = B )
let K be subset-closed SimplicialComplexStr of V; :: thesis: ( K is simplex-join-closed iff for A, B being Subset of K st A is simplex-like & B is simplex-like & Int (@ A) meets Int (@ B) holds
A = B )

hereby :: thesis: ( ( for A, B being Subset of K st A is simplex-like & B is simplex-like & Int (@ A) meets Int (@ B) holds
A = B ) implies K is simplex-join-closed )

assume A1: K is simplex-join-closed ; :: thesis: for A, B being Subset of K st A is simplex-like & B is simplex-like & Int (@ A) meets Int (@ B) holds
not A <> B
let A, B be Subset of K; :: thesis: ( A is simplex-like & B is simplex-like & Int (@ A) meets Int (@ B) implies not A <> B )
assume that
A2: ( A is simplex-like & B is simplex-like ) and
A3: Int (@ A) meets Int (@ B) ; :: thesis: not A <> B
A4: (conv (@ A)) /\ (conv (@ B)) = conv (@ (A /\ B)) by A1, A2;
assume A <> B ; :: thesis: contradiction
then A5: ( A /\ B <> A or A /\ B <> B ) ;
A6: ( A /\ B c= A & A /\ B c= B ) by XBOOLE_1:17;
consider x being object such that
A7: x in Int (@ A) and
A8: x in Int (@ B) by A3, XBOOLE_0:3;
( Int (@ A) c= conv (@ A) & Int (@ B) c= conv (@ B) ) by RLAFFIN2:5;
then A9: x in (conv (@ A)) /\ (conv (@ B)) by A7, A8, XBOOLE_0:def 4;

per cases ( A /\ B c< A or A /\ B c< B ) by A5, A6;

suppose A /\ B c< A ; :: thesis: contradiction

then conv (@ (A /\ B)) misses Int (@ A) by RLAFFIN2:7;
hence contradiction by A4, A7, A9, XBOOLE_0:3; :: thesis: verum

end;

suppose A /\ B c< B ; :: thesis: contradiction

then conv (@ (A /\ B)) misses Int (@ B) by RLAFFIN2:7;
hence contradiction by A4, A8, A9, XBOOLE_0:3; :: thesis: verum

end;

end;

end;

assume A10: for A, B being Subset of K st A is simplex-like & B is simplex-like & Int (@ A) meets Int (@ B) holds
A = B ; :: thesis: K is simplex-join-closed
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
A11: A is simplex-like and
A12: B is simplex-like ; :: thesis: (conv (@ A)) /\ (conv (@ B)) = conv (@ (A /\ B))
A13: (conv (@ A)) /\ (conv (@ B)) c= conv (@ (A /\ B))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (conv (@ A)) /\ (conv (@ B)) or x in conv (@ (A /\ B)) )
A14: the_family_of K is subset-closed ;
assume A15: x in (conv (@ A)) /\ (conv (@ B)) ; :: thesis: x in conv (@ (A /\ B))
then x in conv (@ A) by XBOOLE_0:def 4;
then x in union { (Int a) where a is Subset of V : a c= @ A } by RLAFFIN2:8;
then consider Ia being set such that
A16: x in Ia and
A17: Ia in { (Int a) where a is Subset of V : a c= @ A } by TARSKI:def 4;
consider a being Subset of V such that
A18: Ia = Int a and
A19: a c= @ A by A17;
x in conv (@ B) by A15, XBOOLE_0:def 4;
then x in union { (Int b) where b is Subset of V : b c= @ B } by RLAFFIN2:8;
then consider Ib being set such that
A20: x in Ib and
A21: Ib in { (Int b) where b is Subset of V : b c= @ B } by TARSKI:def 4;
consider b being Subset of V such that
A22: Ib = Int b and
A23: b c= @ B by A21;
reconsider a1 = a, b1 = b as Subset of K by A19, A23, XBOOLE_1:1;
A in the topology of K by A11;
then a1 in the topology of K by A14, A19, CLASSES1:def 1;
then A24: a1 is simplex-like ;
B in the topology of K by A12;
then b1 in the topology of K by A14, A23, CLASSES1:def 1;
then A25: b1 is simplex-like ;
Int (@ a1) meets Int (@ b1) by A16, A18, A20, A22, XBOOLE_0:3;
then a1 = b1 by A10, A24, A25;
then a c= @ (A /\ B) by A19, A23, XBOOLE_1:19;
then A26: conv a c= conv (@ (A /\ B)) by RLAFFIN1:3;
x in conv a by A16, A18, RLAFFIN2:def 1;
hence x in conv (@ (A /\ B)) by A26; :: thesis: verum

end;

( conv (@ (A /\ B)) c= conv (@ A) & conv (@ (A /\ B)) c= conv (@ B) ) by RLAFFIN1:3, XBOOLE_1:17;
then conv (@ (A /\ B)) c= (conv (@ A)) /\ (conv (@ B)) by XBOOLE_1:19;
hence (conv (@ A)) /\ (conv (@ B)) = conv (@ (A /\ B)) by A13; :: thesis: verum