deffunc H₁( set ) -> set = { x where x is Element of S -sequents : [$1,x] in R } ;
B1: for inseqs being set holds H₁(inseqs) in bool (S -sequents)

proof

let inseqs be set ; :: thesis: H₁(inseqs) in bool (S -sequents)

now

let x be set ; :: thesis: ( x in H₁(inseqs) implies x in S -sequents )
assume x in H₁(inseqs) ; :: thesis: x in S -sequents
then consider seq being Element of S -sequents such that
B1: ( seq = x & [inseqs,seq] in R ) ;
thus x in S -sequents by B1; :: thesis: verum

end;

then H₁(inseqs) c= S -sequents by TARSKI:def 3;
hence H₁(inseqs) in bool (S -sequents) ; :: thesis: verum

end;

B2: for inseqs being set st inseqs in bool (S -sequents) holds
H₁(inseqs) in bool (S -sequents) by B1;
consider f being Function of (bool (S -sequents)),(bool (S -sequents)) such that
B3: for x being set st x in bool (S -sequents) holds
f . x = H₁(x) from FUNCT_2:sch 2(B2);
take f ; :: thesis: ( f is Rule of S & ( for inseqs being set st inseqs in bool (S -sequents) holds
f . inseqs = { x where x is Element of S -sequents : [inseqs,x] in R } ) )
thus ( f is Rule of S & ( for inseqs being set st inseqs in bool (S -sequents) holds
f . inseqs = { x where x is Element of S -sequents : [inseqs,x] in R } ) ) by B3, FUNCT_2:8; :: thesis: verum