defpred S₁[ object , object ] means ex x being Element of USS st
( x = $1 & $2 = Neighborhood x );
A1: for x being object st x in the carrier of USS holds
ex y being object st
( y in bool (bool the carrier of USS) & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in the carrier of USS implies ex y being object st
( y in bool (bool the carrier of USS) & S₁[x,y] ) )
assume x in the carrier of USS ; :: thesis: ex y being object st
( y in bool (bool the carrier of USS) & S₁[x,y] )
then reconsider y = x as Element of USS ;
take z = Neighborhood y; :: thesis: ( z in bool (bool the carrier of USS) & S₁[x,z] )
thus z in bool (bool the carrier of USS) ; :: thesis: S₁[x,z]
thus S₁[x,z] ; :: thesis: verum

end;

consider f being Function of the carrier of USS,(bool (bool the carrier of USS)) such that
A2: for x being object st x in the carrier of USS holds
S₁[x,f . x] from FUNCT_2:sch 1(A1);
take f ; :: thesis: for x being Element of USS holds f . x = Neighborhood x

hereby :: thesis: verum

let x be Element of USS; :: thesis: f . x = Neighborhood x
S₁[x,f . x] by A2;
hence f . x = Neighborhood x ; :: thesis: verum

end;