defpred S₁[ set , set ] means $2 in F₃($1);
consider R being Relation of F₂() such that
A2: for x, y being set holds
( [x,y] in R iff ( x in F₂() & y in F₂() & S₁[x,y] ) ) from RELSET_1:sch 1();
take R ; :: thesis: for i being Element of F₁() st i in F₂() holds
Im R,i = F₃(i)
let i be Element of F₁(); :: thesis: ( i in F₂() implies Im R,i = F₃(i) )
assume A3: i in F₂() ; :: thesis: Im R,i = F₃(i)
thus Im R,i c= F₃(i) :: according to XBOOLE_0:def 10 :: thesis: F₃(i) c= Im R,i

proof

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in Im R,i or e in F₃(i) )
assume e in Im R,i ; :: thesis: e in F₃(i)
then consider u being set such that
A4: [u,e] in R and
A5: u in {i} by RELAT_1:def 13;
u = i by A5, TARSKI:def 1;
hence e in F₃(i) by A2, A4; :: thesis: verum

end;

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in F₃(i) or e in Im R,i )
assume A6: e in F₃(i) ; :: thesis: e in Im R,i
F₃(i) c= F₂() by A1, A3;
then ( i in {i} & [i,e] in R ) by A2, A3, A6, TARSKI:def 1;
hence e in Im R,i by RELAT_1:def 13; :: thesis: verum