now :: thesis: for x being object st x in { g where g is PartFunc of X,REAL : ( g in Lp_Functions (M,k) & f a.e.= g,M ) } holds
x in Lp_Functions (M,k)

let x be object ; :: thesis: ( x in { g where g is PartFunc of X,REAL : ( g in Lp_Functions (M,k) & f a.e.= g,M ) } implies x in Lp_Functions (M,k) )
assume x in { g where g is PartFunc of X,REAL : ( g in Lp_Functions (M,k) & f a.e.= g,M ) } ; :: thesis: x in Lp_Functions (M,k)
then ex g being PartFunc of X,REAL st
( x = g & g in Lp_Functions (M,k) & f a.e.= g,M ) ;
hence x in Lp_Functions (M,k) ; :: thesis: verum

end;

hence { h where h is PartFunc of X,REAL : ( h in Lp_Functions (M,k) & f a.e.= h,M ) } is Subset of (Lp_Functions (M,k)) by TARSKI:def 3; :: thesis: verum