let V be RealLinearSpace; :: thesis: for Ks being simplex-join-closed SimplicialComplex of V

for As, Bs being Subset of Ks st As is simplex-like & Bs is simplex-like & Int (@ As) meets conv (@ Bs) holds

As c= Bs

let Ks be simplex-join-closed SimplicialComplex of V; :: thesis: for As, Bs being Subset of Ks st As is simplex-like & Bs is simplex-like & Int (@ As) meets conv (@ Bs) holds

As c= Bs

let As, Bs be Subset of Ks; :: thesis: ( As is simplex-like & Bs is simplex-like & Int (@ As) meets conv (@ Bs) implies As c= Bs )

assume that

A1: As is simplex-like and

A2: Bs is simplex-like and

A3: Int (@ As) meets conv (@ Bs) ; :: thesis: As c= Bs

consider x being object such that

A4: x in Int (@ As) and

A5: x in conv (@ Bs) by A3, XBOOLE_0:3;

x in union { (Int b) where b is Subset of V : b c= @ Bs } by A5, RLAFFIN2:8;

then consider Ib being set such that

A6: x in Ib and

A7: Ib in { (Int b) where b is Subset of V : b c= @ Bs } by TARSKI:def 4;

consider b being Subset of V such that

A8: Ib = Int b and

A9: b c= @ Bs by A7;

reconsider b1 = b as Subset of Ks by A9, XBOOLE_1:1;

As in the topology of Ks by A1;

then not Ks is void by PENCIL_1:def 4;

then A10: b1 is simplex-like by A2, A9, MATROID0:1;

Int (@ As) meets Int (@ b1) by A4, A6, A8, XBOOLE_0:3;

hence As c= Bs by A1, A9, A10, Th25; :: thesis: verum

for As, Bs being Subset of Ks st As is simplex-like & Bs is simplex-like & Int (@ As) meets conv (@ Bs) holds

As c= Bs

let Ks be simplex-join-closed SimplicialComplex of V; :: thesis: for As, Bs being Subset of Ks st As is simplex-like & Bs is simplex-like & Int (@ As) meets conv (@ Bs) holds

As c= Bs

let As, Bs be Subset of Ks; :: thesis: ( As is simplex-like & Bs is simplex-like & Int (@ As) meets conv (@ Bs) implies As c= Bs )

assume that

A1: As is simplex-like and

A2: Bs is simplex-like and

A3: Int (@ As) meets conv (@ Bs) ; :: thesis: As c= Bs

consider x being object such that

A4: x in Int (@ As) and

A5: x in conv (@ Bs) by A3, XBOOLE_0:3;

x in union { (Int b) where b is Subset of V : b c= @ Bs } by A5, RLAFFIN2:8;

then consider Ib being set such that

A6: x in Ib and

A7: Ib in { (Int b) where b is Subset of V : b c= @ Bs } by TARSKI:def 4;

consider b being Subset of V such that

A8: Ib = Int b and

A9: b c= @ Bs by A7;

reconsider b1 = b as Subset of Ks by A9, XBOOLE_1:1;

As in the topology of Ks by A1;

then not Ks is void by PENCIL_1:def 4;

then A10: b1 is simplex-like by A2, A9, MATROID0:1;

Int (@ As) meets Int (@ b1) by A4, A6, A8, XBOOLE_0:3;

hence As c= Bs by A1, A9, A10, Th25; :: thesis: verum