set M = { (- s) where s is Element of L : s in S } ;

now :: thesis: for x being object st x in { (- s) where s is Element of L : s in S } holds
x in the carrier of L

let x be object ; :: thesis: ( x in { (- s) where s is Element of L : s in S } implies x in the carrier of L )
assume x in { (- s) where s is Element of L : s in S } ; :: thesis: x in the carrier of L
then consider s being Element of L such that
A1: ( x = - s & s in S ) ;
thus x in the carrier of L by A1; :: thesis: verum

end;

then { (- s) where s is Element of L : s in S } c= the carrier of L ;
hence { (- s) where s is Element of L : s in S } is Subset of L ; :: thesis: verum