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

proof

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

end;

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