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