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

now

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

now

let x be set ; :: thesis: ( x in (R8 S) . Seqts implies x in (R8 S) . Seqts2 )
assume CC0: x in (R8 S) . Seqts ; :: thesis: x in (R8 S) . Seqts2
reconsider seqt = x as Element of S -sequents by CC0;
[Seqts,seqt] in P8 S by CC0, Lm1e;
then seqt Rule8 Seqts by DefP8;
then consider y1, y2 being set , phi, phi1, phi2 being wff string of S such that
C1: ( y1 in Seqts & y2 in Seqts & y1 `1 = y2 `1 & y1 `2 = phi1 & y2 `2 = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 & {phi} \/ (seqt `1) = y1 `1 & seqt `2 = (<*(TheNorSymbOf S)*> ^ phi) ^ phi ) by Def8;
seqt Rule8 Seqts2 by Def8, C1, B0;
then [Seqts2,seqt] in P8 S by DefP8;
hence x in (R8 S) . Seqts2 by Th3; :: thesis: verum

end;

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

end;

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