set Y = { (v + u) where u is Element of V : u in W } ;

defpred S_{1}[ object ] means ex u being Element of V st

( $1 = v + u & u in W );

consider X being set such that

A1: for x being object holds

( x in X iff ( x in the carrier of V & S_{1}[x] ) )
from XBOOLE_0:sch 1();

for x being object st x in X holds

x in the carrier of V by A1;

then reconsider X = X as Subset of V by TARSKI:def 3;

A2: { (v + u) where u is Element of V : u in W } c= X

defpred S

( $1 = v + u & u in W );

consider X being set such that

A1: for x being object holds

( x in X iff ( x in the carrier of V & S

for x being object st x in X holds

x in the carrier of V by A1;

then reconsider X = X as Subset of V by TARSKI:def 3;

A2: { (v + u) where u is Element of V : u in W } c= X

proof

X c= { (v + u) where u is Element of V : u in W }
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (v + u) where u is Element of V : u in W } or x in X )

assume x in { (v + u) where u is Element of V : u in W } ; :: thesis: x in X

then ex u being Element of V st

( x = v + u & u in W ) ;

hence x in X by A1; :: thesis: verum

end;assume x in { (v + u) where u is Element of V : u in W } ; :: thesis: x in X

then ex u being Element of V st

( x = v + u & u in W ) ;

hence x in X by A1; :: thesis: verum

proof

hence
{ (v + u) where u is Element of V : u in W } is Subset of V
by A2, XBOOLE_0:def 10; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in { (v + u) where u is Element of V : u in W } )

assume x in X ; :: thesis: x in { (v + u) where u is Element of V : u in W }

then ex u being Element of V st

( x = v + u & u in W ) by A1;

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

end;assume x in X ; :: thesis: x in { (v + u) where u is Element of V : u in W }

then ex u being Element of V st

( x = v + u & u in W ) by A1;

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