theorem :: LPSPACE2:32

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for k being positive Real holds
( 0. (RLSp_LpFunct (M,k)) = X --> 0 & 0. (RLSp_LpFunct (M,k)) in AlmostZeroLpFunctions (M,k) )