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