defpred S₁[ set , set , set ] means for B being Subset of T st B = $2 holds
$3 = B ^b ;
A1: for n being Element of NAT
for x being Subset of T ex y being Subset of T st S₁[n,x,y]

proof

let n be Element of NAT ; :: thesis: for x being Subset of T ex y being Subset of T st S₁[n,x,y]
let x be Subset of T; :: thesis: ex y being Subset of T st S₁[n,x,y]
reconsider C = x as Subset of T ;
S₁[n,x,C ^b ] ;
hence ex y being Subset of T st S₁[n,x,y] ; :: thesis: verum

end;

ex f being Function of NAT ,(bool the carrier of T) st
( f . 0 = A & ( for n being Element of NAT holds S₁[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch 2(A1);
hence ex b₁ being Function of NAT ,(bool the carrier of T) st
( ( for n being Element of NAT
for B being Subset of T st B = b₁ . n holds
b₁ . (n + 1) = B ^b ) & b₁ . 0 = A ) ; :: thesis: verum