set t = the finite Tree;
take <* the finite Tree*> ; :: thesis: ( <* the finite Tree*> is V32() & <* the finite Tree*> is Tree-yielding & not <* the finite Tree*> is empty )
thus <* the finite Tree*> is V32() :: thesis: ( <* the finite Tree*> is Tree-yielding & not <* the finite Tree*> is empty )
proof
now :: thesis: for x being set st x in rng <* the finite Tree*> holds
x is finite
let x be set ; :: thesis: ( x in rng <* the finite Tree*> implies x is finite )
assume x in rng <* the finite Tree*> ; :: thesis: x is finite
then x in { the finite Tree} by FINSEQ_1:39;
hence x is finite ; :: thesis: verum
end;
hence <* the finite Tree*> is V32() ; :: thesis: verum
end;
thus ( <* the finite Tree*> is Tree-yielding & not <* the finite Tree*> is empty ) ; :: thesis: verum