set R = R#4 S;
set Q = S -sequents ;

now :: thesis: for Seqts, Seqts2 being Subset of (S -sequents) st Seqts c= Seqts2 holds
(R#4 S) . Seqts c= (R#4 S) . Seqts2

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

now :: thesis: for x being set st x in (R#4 S) . Seqts holds
x in (R#4 S) . Seqts2

let x be set ; :: thesis: ( x in (R#4 S) . Seqts implies x in (R#4 S) . Seqts2 )
assume A1: x in (R#4 S) . Seqts ; :: thesis: x in (R#4 S) . Seqts2
reconsider seqt = x as Element of S -sequents by A1;
[Seqts,seqt] in P#4 S by A1, Lm29;
then seqt Rule4 Seqts by Def38;
then consider l being literal Element of S, phi being wff string of S, t being termal string of S such that
A2: ( seqt `1 = {((l,t) SubstIn phi)} & seqt `2 = <*l*> ^ phi ) by Def25;
seqt Rule4 Seqts2 by A2, Def25;
then [Seqts2,seqt] in P#4 S by Def38;
hence x in (R#4 S) . Seqts2 by Th2; :: thesis: verum

end;

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

end;

hence for b₁ being Rule of S st b₁ = R#4 S holds
b₁ is isotone by Def9; :: thesis: verum