take bool (NAT *) ; :: thesis: for b₁ being Tree holds b₁ in bool (NAT *)
let d be Tree; :: thesis: d in bool (NAT *)
d c= NAT * by TREES_1:def 3;
hence d in bool (NAT *) ; :: thesis: verum