defpred S₁[ object , object ] means ( $1 = $2 & ex S being Relation st
( S = $2 & P₁[S] ) );
A1: for y, t, v being object st S₁[y,t] & S₁[y,v] holds
t = v ;
consider B being set such that
A2: for t being object holds
( t in B iff ex y being object st
( y in F₁() & S₁[y,t] ) ) from TARSKI:sch 1(A1);
take B ; :: thesis: for R being Relation holds
( R in B iff ( R in F₁() & P₁[R] ) )
let R be Relation; :: thesis: ( R in B iff ( R in F₁() & P₁[R] ) )
( R in B implies ex T being Relation st
( T in F₁() & T = R & P₁[R] ) )

proof

assume R in B ; :: thesis: ex T being Relation st
( T in F₁() & T = R & P₁[R] )
then consider y being object such that
A3: y in F₁() and
A4: y = R and
A5: ex S being Relation st
( S = R & P₁[S] ) by A2;
reconsider y = y as Relation by A4;
take y ; :: thesis: ( y in F₁() & y = R & P₁[R] )
thus ( y in F₁() & y = R & P₁[R] ) by A3, A4, A5; :: thesis: verum

end;

hence ( R in B implies ( R in F₁() & P₁[R] ) ) ; :: thesis: ( R in F₁() & P₁[R] implies R in B )
thus ( R in F₁() & P₁[R] implies R in B ) by A2; :: thesis: verum