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

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

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

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

let x be object ; :: thesis: ( x in (R#5 S) . Seqts implies x in (R#5 S) . Seqts2 )
assume A2: x in (R#5 S) . Seqts ; :: thesis: x in (R#5 S) . Seqts2
reconsider seqt = x as Element of S -sequents by A2;
[Seqts,seqt] in P#5 S by A2, Lm30;
then seqt Rule5 Seqts by Def42;
then consider v1, v2 being literal Element of S, z being set , p being FinSequence such that
A3: ( seqt `1 = z \/ {(<*v1*> ^ p)} & v2 is (z \/ {p}) \/ {(seqt `2)} -absent & [(z \/ {((v1 SubstWith v2) . p)}),(seqt `2)] in Seqts ) ;
seqt Rule5 Seqts2 by A1, A3;
then [Seqts2,seqt] in P#5 S by Def42;
hence x in (R#5 S) . Seqts2 by Th3; :: thesis: verum

end;

hence (R#5 S) . Seqts c= (R#5 S) . Seqts2 ; :: thesis: verum

end;

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