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))

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

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

X --> 0 in Lp_Functions (M,k)
by Th23;
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;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

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