take Kr ; :: thesis: ( |.Kr.| c= |.Kr.| & ( for A being Subset of Kr st A is simplex-like holds
ex B being Subset of Kr st
( B is simplex-like & conv (@ A) c= conv (@ B) ) ) )
thus ( |.Kr.| c= |.Kr.| & ( for A being Subset of Kr st A is simplex-like holds
ex B being Subset of Kr st
( B is simplex-like & conv (@ A) c= conv (@ B) ) ) ) ; :: thesis: verum