:: deftheorem Def18 defines Pre-L-Space LPSPACE1:def 18 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for b₄ being non empty right_complementable strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct holds
( b₄ = Pre-L-Space M iff ( the carrier of b₄ = CosetSet M & the addF of b₄ = addCoset M & 0. b₄ = zeroCoset M & the Mult of b₄ = lmultCoset M ) );