defpred S₁[ object , object ] means for X being set st $1 = X holds
$2 = R .: X;
A1: for x being object st x in bool A holds
ex y being object st S₁[x,y]

proof

let x be object ; :: thesis: ( x in bool A implies ex y being object st S₁[x,y] )
assume x in bool A ; :: thesis: ex y being object st S₁[x,y]
reconsider x = x as set by TARSKI:1;
take R .: x ; :: thesis: S₁[x,R .: x]
thus S₁[x,R .: x] ; :: thesis: verum

end;

consider g being Function such that
A2: dom g = bool A and
A3: for x being object st x in bool A holds
S₁[x,g . x] from CLASSES1:sch 1(A1);
take g ; :: thesis: ( dom g = bool A & ( for X being set st X c= A holds
g . X = R .: X ) )
thus ( dom g = bool A & ( for X being set st X c= A holds
g . X = R .: X ) ) by A2, A3; :: thesis: verum