let W be Tree; :: thesis: W = union { (W -level n) where n is Element of NAT : verum }
thus W c= union { (W -level n) where n is Element of NAT : verum } :: according to XBOOLE_0:def 10 :: thesis: union { (W -level n) where n is Element of NAT : verum } 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 : verum } )
assume A1: x in W ; :: thesis: x in union { (W -level n) where n is Element of NAT : verum }
reconsider w = x as Element of W by A1;
A2: x in W -level (len w) ;
A3: W -level (len w) in { (W -level n) where n is Element of NAT : verum } ;
thus x in union { (W -level n) where n is Element of NAT : verum } by A2, 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 : verum } or x in W )
assume A4: x in union { (W -level n) where n is Element of NAT : verum } ; :: thesis: x in W
consider X being set such that
A5: ( x in X & X in { (W -level n) where n is Element of NAT : verum } ) by A4, TARSKI:def 4;
A6: ex n being Element of NAT st X = W -level n by A5;
thus x in W by A5, A6; :: thesis: verum