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

proof

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

end;

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