let W be finite Tree; :: thesis: W = union { (W -level n) where n is Nat : n <= height W }
thus W c= union { (W -level n) where n is Nat : n <= height W } :: according to XBOOLE_0:def 10 :: thesis: union { (W -level n) where n is Nat : n <= height W } c= W

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in W or x in union { (W -level n) where n is Nat : n <= height W } )
assume x in W ; :: thesis: x in union { (W -level n) where n is Nat : n <= height W }
then reconsider w = x as Element of W ;
A1: len w <= height W by TREES_1:def 12;
A2: w in W -level (len w) ;
W -level (len w) in { (W -level n) where n is Nat : n <= height W } by A1;
hence x in union { (W -level n) where n is Nat : n <= height W } by A2, TARSKI:def 4; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union { (W -level n) where n is Nat : n <= height W } or x in W )
assume x in union { (W -level n) where n is Nat : n <= height W } ; :: thesis: x in W
then consider X being set such that
A3: ( x in X & X in { (W -level n) where n is Nat : n <= height W } ) by TARSKI:def 4;
ex n being Nat st
( X = W -level n & n <= height W ) by A3;
hence x in W by A3; :: thesis: verum