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 ;
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 ;
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 ; :: 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 ;
hence x in |.K.| by ; :: thesis: verum