defpred S₁[ Real] means ex z being Real st
( z in A & $1 = x + z );
ex B being Subset of REAL st
for y being Real holds
( y in B iff S₁[y] ) from SUBSET_1:sch 3();
hence ex b₁ being Subset of REAL st
for y being Real holds
( y in b₁ iff ex z being Real st
( z in A & y = x + z ) ) ; :: thesis: verum