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₁( Element of V) -> Element of the carrier of V = r * $1;
card { H₁(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