set C = { (a.e-eq-class_Lp f,M,k) where f is PartFunc of X,REAL : f in Lp_Functions M,k } ;
A1: { (a.e-eq-class_Lp f,M,k) where f is PartFunc of X,REAL : f in Lp_Functions M,k } c= bool (Lp_Functions M,k)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (a.e-eq-class_Lp f,M,k) where f is PartFunc of X,REAL : f in Lp_Functions M,k } or x in bool (Lp_Functions M,k) )
assume x in { (a.e-eq-class_Lp f,M,k) where f is PartFunc of X,REAL : f in Lp_Functions M,k } ; :: thesis: x in bool (Lp_Functions M,k)
then ex f being PartFunc of X,REAL st
( a.e-eq-class_Lp f,M,k = x & f in Lp_Functions M,k ) ;
hence x in bool (Lp_Functions M,k) ; :: thesis: verum

end;

X --> 0 in Lp_Functions M,k by LmDef1Lp;
then a.e-eq-class_Lp (X --> 0 ),M,k in { (a.e-eq-class_Lp f,M,k) where f is PartFunc of X,REAL : f in Lp_Functions M,k } ;
hence { (a.e-eq-class_Lp f,M,k) where f is PartFunc of X,REAL : f in Lp_Functions M,k } is non empty Subset-Family of (Lp_Functions M,k) by A1; :: thesis: verum