defpred S₁[ set , set ] means ex o being OperSymbol of S st
( the_result_sort_of o = $2 & ex i being Element of NAT st
( i in dom (the_arity_of o) & (the_arity_of o) /. i = $1 ) );
ex R being Relation of the carrier of S, the carrier of S st
for x, y being SortSymbol of S holds
( [x,y] in R iff S₁[x,y] ) from RELSET_1:sch 2();
hence ex b₁ being Relation of the carrier of S st
for s1, s2 being SortSymbol of S holds
( [s1,s2] in b₁ iff ex o being OperSymbol of S st
( the_result_sort_of o = s2 & ex i being Element of NAT st
( i in dom (the_arity_of o) & (the_arity_of o) /. i = s1 ) ) ) ; :: thesis: verum