{ (w ^ <*n*>) where n is Nat : w ^ <*n*> in W } c= W

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (w ^ <*n*>) where n is Nat : w ^ <*n*> in W } or x in W )
assume x in { (w ^ <*n*>) where n is Nat : w ^ <*n*> in W } ; :: thesis: x in W
then ex n being Nat st
( x = w ^ <*n*> & w ^ <*n*> in W ) ;
hence x in W ; :: thesis: verum

end;

hence { (w ^ <*n*>) where n is Nat : w ^ <*n*> in W } is Subset of W ; :: thesis: verum