A2: card { F₄(w) where w is Element of F₁() : w in F₂() } c= card F₂() from TREES_2:sch 2();
thus card F₃() <= card F₂() by A1, A2, NAT_1:40; :: thesis: verum