A8: { (w ^ <*n*>) where n is Element of NAT : w ^ <*n*> in W } c= W

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (w ^ <*n*>) where n is Element of NAT : w ^ <*n*> in W } or x in W )
assume A9: x in { (w ^ <*n*>) where n is Element of NAT : w ^ <*n*> in W } ; :: thesis: x in W
A10: ex n being Element of NAT st
( x = w ^ <*n*> & w ^ <*n*> in W ) by A9;
thus x in W by A10; :: thesis: verum

end;

thus { (w ^ <*n*>) where n is Element of NAT : w ^ <*n*> in W } is Subset of W by A8; :: thesis: verum