let V be RealLinearSpace; :: thesis: for Ks being simplex-join-closed SimplicialComplex of V
for As, Bs being Subset of Ks st not As is dependent & not Bs is dependent & 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 not As is dependent & not Bs is dependent & Int (@ As) meets conv (@ Bs) holds
As c= Bs
let As, Bs be Subset of Ks; :: thesis: ( not As is dependent & not Bs is dependent & Int (@ As) meets conv (@ Bs) implies As c= Bs )
assume that
A1: not As is dependent and
A2: not Bs is dependent and
A3: Int (@ As) meets conv (@ Bs) ; :: thesis: As c= Bs
consider x being set 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, PRE_TOPC:def 2;
then not Ks is void by PENCIL_1:def 4;
then A10: not b1 is dependent 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