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 object ; :: 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 Th23;
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