set r = { (T . t) where t is Node of T : t <> {} } ;
{ (T . t) where t is Node of T : t <> {} } c= rng T

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (T . t) where t is Node of T : t <> {} } or x in rng T )
assume x in { (T . t) where t is Node of T : t <> {} } ; :: thesis: x in rng T
then ex t being Node of T st
( x = T . t & t <> {} ) ;
hence x in rng T by FUNCT_1:3; :: thesis: verum

end;

hence { (T . t) where t is Node of T : t <> {} } is finite Subset of [:(LTLB_WFF **),(LTLB_WFF **):] by XBOOLE_1:1; :: thesis: verum