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 ;
TARSKI:def 3 ( 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) }
;
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))
;
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; verum