defpred S₁[ set ] means ex u being Element of V st
( $1 = v + u & u in M );
consider X being set such that
A1: for x being set holds
( x in X iff ( x in the carrier of V & S₁[x] ) ) from XBOOLE_0:sch 1();
X c= the carrier of V

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in the carrier of V )
assume x in X ; :: thesis: x in the carrier of V
hence x in the carrier of V by A1; :: thesis: verum

end;

then reconsider X = X as Subset of V ;
reconsider X = X as Subset of V ;
set Y = { (v + u) where u is Element of V : u in M } ;
X = { (v + u) where u is Element of V : u in M }

proof

thus X c= { (v + u) where u is Element of V : u in M } :: according to XBOOLE_0:def 10 :: thesis: { (v + u) where u is Element of V : u in M } c= X

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in { (v + u) where u is Element of V : u in M } )
assume x in X ; :: thesis: x in { (v + u) where u is Element of V : u in M }
then ex u being Element of V st
( x = v + u & u in M ) by A1;
hence x in { (v + u) where u is Element of V : u in M } ; :: thesis: verum

end;

thus { (v + u) where u is Element of V : u in M } c= X :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (v + u) where u is Element of V : u in M } or x in X )
assume x in { (v + u) where u is Element of V : u in M } ; :: thesis: x in X
then ex u being Element of V st
( x = v + u & u in M ) ;
hence x in X by A1; :: thesis: verum

end;

end;

hence { (v + u) where u is Element of V : u in M } is Subset of V ; :: thesis: verum