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) ) )

hereby :: thesis: ( ex A being Subset of K st
( 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;

given A being Subset of K such that A7: A is simplex-like and
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