X --> 0 in Lp_Functions (M,k) by Th23;
then a.e-eq-class_Lp ((X --> 0),M,k) in CosetSet (M,k) ;
hence a.e-eq-class_Lp ((X --> 0),M,k) is Element of CosetSet (M,k) ; :: thesis: verum