set Y = { (v + u) where u is Element of V : u in W } ;
defpred S1[ 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 & S1[x] ) ) from 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
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;
X c= { (v + u) where u is Element of V : u in W }
proof
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;
hence { (v + u) where u is Element of V : u in W } is Subset of V by ; :: thesis: verum