let V be non empty RLSStruct ; :: thesis: for A being Subset of V

for r being Real holds card (r * A) c= card A

let A be Subset of V; :: thesis: for r being Real holds card (r * A) c= card A

let r be Real; :: thesis: card (r * A) c= card A

deffunc H_{1}( Element of V) -> Element of the carrier of V = r * $1;

card { H_{1}(w) where w is Element of V : w in A } c= card A
from TREES_2:sch 2();

hence card (r * A) c= card A by CONVEX1:def 1; :: thesis: verum

for r being Real holds card (r * A) c= card A

let A be Subset of V; :: thesis: for r being Real holds card (r * A) c= card A

let r be Real; :: thesis: card (r * A) c= card A

deffunc H

card { H

hence card (r * A) c= card A by CONVEX1:def 1; :: thesis: verum