defpred S₁[ set ] means ex z being Real st
( z in A & $1 = x * z );
consider B being Subset of REAL such that
A1: for y being Real holds
( y in B iff S₁[y] ) from SUBSET_1:sch 3();
reconsider B = B as Subset of REAL ;
take B ; :: thesis: for y being Real holds
( y in B iff ex z being Real st
( z in A & y = x * z ) )
thus for y being Real holds
( y in B iff ex z being Real st
( z in A & y = x * z ) ) by A1; :: thesis: verum