let T be non empty TopSpace; :: thesis: for s being Function of , the carrier of T
for M being Subset of the carrier of T holds
( s " M in iff ex n being Nat st square-uparrow n c= s " M )

let s be Function of , the carrier of T; :: thesis: for M being Subset of the carrier of T holds
( s " M in iff ex n being Nat st square-uparrow n c= s " M )

let M be Subset of the carrier of T; :: thesis: ( s " M in iff ex n being Nat st square-uparrow n c= s " M )
hereby :: thesis: ( ex n being Nat st square-uparrow n c= s " M implies s " M in )
assume s " M in ; :: thesis: ex n being Nat st square-uparrow n c= s " M
then consider b being Element of such that
A1: b c= s " M by ;
ex n being Nat st square-uparrow n c= b by Th32;
hence ex n being Nat st square-uparrow n c= s " M by ; :: thesis: verum
end;
given n being Nat such that A2: square-uparrow n c= s " M ; :: thesis:
square-uparrow n in { () where n is Nat : verum } ;
then ex b2 being Element of st b2 c= square-uparrow n by Th34;
then A3: ex b2 being Element of st b2 c= s " M by ;
dom s = by FUNCT_2:def 1;
then s " M is Subset of by RELAT_1:132;
hence s " M in by ; :: thesis: verum