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

proof

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

end;

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