let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in |.K.| ; :: thesis:
then consider S being Subset of K such that
A4: S is simplex-like and
A5: x in conv (@ S) by Def3;
reconsider S1 = @ S as non empty Subset of V by A5;
x in { (Sum L) where L is Convex_Combination of S1 : L in ConvexComb V } by A5, CONVEX3:5;
then consider L being Convex_Combination of S1 such that
A6: ( x = Sum L & L in ConvexComb V ) ;
reconsider Carr = Carrier L as non empty Subset of V by CONVEX1:21;
A7: Carr c= S by RLVECT_2:def 6;
then reconsider Carr1 = Carr as Subset of C by XBOOLE_1:1;
S in the topology of K by A4;
then Carr1 in the topology of K by A2, A7, CLASSES1:def 1;
then Carr1 in the topology of C by A1, A3, COHSP_1:def 3;
then A8: Carr1 is simplex-like ;
reconsider LC = L as Linear_Combination of Carr by RLVECT_2:def 6;
LC is convex ;
then x in { (Sum M) where M is Convex_Combination of Carr : M in ConvexComb V } by A6;
then A9: x in conv Carr by CONVEX3:5;
Carr = @ Carr1 ;
hence x in |.C.| by A8, A9, Def3; :: thesis:

end;

end;