set R1 = the Relation;
set I = the carrier of R;
set f = the carrier of R --> the Relation;
reconsider f = the carrier of R --> the Relation as ManySortedSet of the carrier of R ;
f is order-sorted

proof

let s1, s2 be Element of R; :: according to OSALG_1:def 16 :: thesis: ( not s1 <= s2 or f . s1 c= f . s2 )
assume s1 <= s2 ; :: thesis: f . s1 c= f . s2
f . s1 = the Relation by FUNCOP_1:7;
hence f . s1 c= f . s2 by FUNCOP_1:7; :: thesis: verum

end;

then reconsider f = f as OrderSortedSet of R ;
take f ; :: thesis: f is Relation-yielding
for x being set st x in dom f holds
f . x is Relation by FUNCOP_1:7;
hence f is Relation-yielding by FUNCOP_1:def 11; :: thesis: verum