let x be set ; :: thesis: for V being RealLinearSpace

for K being subset-closed SimplicialComplexStr of V holds

( x in |.K.| iff ex A being Subset of K st

( A is simplex-like & x in Int (@ A) ) )

let V be RealLinearSpace; :: thesis: for K being subset-closed SimplicialComplexStr of V holds

( x in |.K.| iff ex A being Subset of K st

( A is simplex-like & x in Int (@ A) ) )

let K be subset-closed SimplicialComplexStr of V; :: thesis: ( x in |.K.| iff ex A being Subset of K st

( A is simplex-like & x in Int (@ A) ) )

A8: x in Int (@ A) ; :: thesis: x in |.K.|

x in conv (@ A) by A8, RLAFFIN2:def 1;

hence x in |.K.| by A7, Def3; :: thesis: verum

for K being subset-closed SimplicialComplexStr of V holds

( x in |.K.| iff ex A being Subset of K st

( A is simplex-like & x in Int (@ A) ) )

let V be RealLinearSpace; :: thesis: for K being subset-closed SimplicialComplexStr of V holds

( x in |.K.| iff ex A being Subset of K st

( A is simplex-like & x in Int (@ A) ) )

let K be subset-closed SimplicialComplexStr of V; :: thesis: ( x in |.K.| iff ex A being Subset of K st

( A is simplex-like & x in Int (@ A) ) )

hereby :: thesis: ( ex A being Subset of K st

( A is simplex-like & x in Int (@ A) ) implies x in |.K.| )

given A being Subset of K such that A7:
A is simplex-like
and ( A is simplex-like & x in Int (@ A) ) implies x in |.K.| )

assume
x in |.K.|
; :: thesis: ex B1 being Subset of K st

( B1 is simplex-like & x in Int (@ B1) )

then consider A being Subset of K such that

A1: A is simplex-like and

A2: x in conv (@ A) by Def3;

conv (@ A) = union { (Int B) where B is Subset of V : B c= @ A } by RLAFFIN2:8;

then consider IB being set such that

A3: x in IB and

A4: IB in { (Int B) where B is Subset of V : B c= @ A } by A2, TARSKI:def 4;

consider B being Subset of V such that

A5: IB = Int B and

A6: B c= @ A by A4;

reconsider B1 = B as Subset of K by A6, XBOOLE_1:1;

take B1 = B1; :: thesis: ( B1 is simplex-like & x in Int (@ B1) )

A in the topology of K by A1;

then not K is void by PENCIL_1:def 4;

hence ( B1 is simplex-like & x in Int (@ B1) ) by A1, A3, A5, A6, MATROID0:1; :: thesis: verum

end;( B1 is simplex-like & x in Int (@ B1) )

then consider A being Subset of K such that

A1: A is simplex-like and

A2: x in conv (@ A) by Def3;

conv (@ A) = union { (Int B) where B is Subset of V : B c= @ A } by RLAFFIN2:8;

then consider IB being set such that

A3: x in IB and

A4: IB in { (Int B) where B is Subset of V : B c= @ A } by A2, TARSKI:def 4;

consider B being Subset of V such that

A5: IB = Int B and

A6: B c= @ A by A4;

reconsider B1 = B as Subset of K by A6, XBOOLE_1:1;

take B1 = B1; :: thesis: ( B1 is simplex-like & x in Int (@ B1) )

A in the topology of K by A1;

then not K is void by PENCIL_1:def 4;

hence ( B1 is simplex-like & x in Int (@ B1) ) by A1, A3, A5, A6, MATROID0:1; :: thesis: verum

A8: x in Int (@ A) ; :: thesis: x in |.K.|

x in conv (@ A) by A8, RLAFFIN2:def 1;

hence x in |.K.| by A7, Def3; :: thesis: verum