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