set R = R9 S;
set Q = S -sequents ;

now

let Seqts, Seqts2 be Subset of (S -sequents); :: thesis: ( Seqts c= Seqts2 implies (R9 S) . Seqts c= (R9 S) . Seqts2 )
set X = Seqts;
set Y = Seqts2;
assume B0: Seqts c= Seqts2 ; :: thesis: (R9 S) . Seqts c= (R9 S) . Seqts2

now

let x be set ; :: thesis: ( x in (R9 S) . Seqts implies x in (R9 S) . Seqts2 )
assume CC0: x in (R9 S) . Seqts ; :: thesis: x in (R9 S) . Seqts2
then C0: ( x in S -sequents & [Seqts,x] in P9 S ) by Lm1e;
reconsider seqt = x as Element of S -sequents by CC0;
seqt Rule9 Seqts by C0, DefP9;
then consider y being set , phi being wff string of S such that
C1: ( y in Seqts & seqt `2 = phi & y `1 = seqt `1 & y `2 = xnot (xnot phi) ) by Def9;
seqt Rule9 Seqts2 by C1, Def9, B0;
then [Seqts2,seqt] in P9 S by DefP9;
hence x in (R9 S) . Seqts2 by Th3; :: thesis: verum

end;

hence (R9 S) . Seqts c= (R9 S) . Seqts2 by TARSKI:def 3; :: thesis: verum

end;

hence for b₁ being Rule of S st b₁ = R9 S holds
b₁ is isotone by DefMonotonic1; :: thesis: verum