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