defpred S1[ object , object ] means ( $1 = $2 & ex S being Relation st
( S = $2 & P1[S] ) );
A1:
for y, t, v being object st S1[y,t] & S1[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 F1() & S1[y,t] ) )
from TARSKI:sch 1(A1);
take
B
; for R being Relation holds
( R in B iff ( R in F1() & P1[R] ) )
let R be Relation; ( R in B iff ( R in F1() & P1[R] ) )
( R in B implies ex T being Relation st
( T in F1() & T = R & P1[R] ) )
proof
assume
R in B
;
ex T being Relation st
( T in F1() & T = R & P1[R] )
then consider y being
object such that A3:
y in F1()
and A4:
y = R
and A5:
ex
S being
Relation st
(
S = R &
P1[
S] )
by A2;
reconsider y =
y as
Relation by A4;
take
y
;
( y in F1() & y = R & P1[R] )
thus
(
y in F1() &
y = R &
P1[
R] )
by A3, A4, A5;
verum
end;
hence
( R in B implies ( R in F1() & P1[R] ) )
; ( R in F1() & P1[R] implies R in B )
thus
( R in F1() & P1[R] implies R in B )
by A2; verum