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 & @ As is affinely-independent & Bs is simplex-like holds

( Int (@ As) c= conv (@ Bs) iff 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 & @ As is affinely-independent & Bs is simplex-like holds

( Int (@ As) c= conv (@ Bs) iff As c= Bs )

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

assume that

A1: As is simplex-like and

A2: @ As is affinely-independent and

A3: Bs is simplex-like ; :: thesis: ( Int (@ As) c= conv (@ Bs) iff As c= Bs )

As in the topology of Ks by A1;

then A4: not Ks is void by PENCIL_1:def 4;

for As, Bs being Subset of Ks st As is simplex-like & @ As is affinely-independent & Bs is simplex-like holds

( Int (@ As) c= conv (@ Bs) iff 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 & @ As is affinely-independent & Bs is simplex-like holds

( Int (@ As) c= conv (@ Bs) iff As c= Bs )

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

assume that

A1: As is simplex-like and

A2: @ As is affinely-independent and

A3: Bs is simplex-like ; :: thesis: ( Int (@ As) c= conv (@ Bs) iff As c= Bs )

As in the topology of Ks by A1;

then A4: not Ks is void by PENCIL_1:def 4;

per cases
( As is empty or not As is empty )
;

end;

suppose
not As is empty
; :: thesis: ( Int (@ As) c= conv (@ Bs) iff As c= Bs )

then
not Int (@ As) is empty
by A1, A2, A4, RLAFFIN2:20;

then consider x being object such that

A6: x in Int (@ As) ;

then ( Int (@ As) c= conv (@ As) & conv (@ As) c= conv (@ Bs) ) by RLAFFIN1:3, RLAFFIN2:5;

hence Int (@ As) c= conv (@ Bs) ; :: thesis: verum

end;then consider x being object such that

A6: x in Int (@ As) ;

hereby :: thesis: ( As c= Bs implies Int (@ As) c= conv (@ Bs) )

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

then x in conv (@ Bs) by A6;

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

then consider Ib being set such that

A7: x in Ib and

A8: 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

A9: Ib = Int b and

A10: b c= @ Bs by A8;

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

A11: b1 is simplex-like by A3, A4, A10, MATROID0:1;

Int (@ As) meets Int (@ b1) by A6, A7, A9, XBOOLE_0:3;

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

end;then x in conv (@ Bs) by A6;

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

then consider Ib being set such that

A7: x in Ib and

A8: 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

A9: Ib = Int b and

A10: b c= @ Bs by A8;

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

A11: b1 is simplex-like by A3, A4, A10, MATROID0:1;

Int (@ As) meets Int (@ b1) by A6, A7, A9, XBOOLE_0:3;

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

then ( Int (@ As) c= conv (@ As) & conv (@ As) c= conv (@ Bs) ) by RLAFFIN1:3, RLAFFIN2:5;

hence Int (@ As) c= conv (@ Bs) ; :: thesis: verum