let V be non empty addLoopStr ; :: thesis: for A being Subset of V
for v being Element of V holds card (v + A) c= card A
let A be Subset of V; :: thesis: for v being Element of V holds card (v + A) c= card A
let v be Element of V; :: thesis: card (v + A) c= card A
deffunc H₁( Element of V) -> Element of the carrier of V = v + $1;
card { H₁(w) where w is Element of V : w in A } c= card A from TREES_2:sch 2();
hence card (v + A) c= card A ; :: thesis: verum