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