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

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

now :: thesis: for x being set st x in (R#3d S) . Seqts1 holds
x in (R#3d S) . Seqts2

let x be set ; :: thesis: ( x in (R#3d S) . Seqts1 implies x in (R#3d S) . Seqts2 )
assume A5: x in (R#3d S) . Seqts1 ; :: thesis: x in (R#3d S) . Seqts2
reconsider seqt = x as Element of S -sequents by A5;
[Seqts1,seqt] in P#3d S by A5, Lm29;
then seqt Rule3d Seqts1 by Def36;
then ex s being low-compounding Element of S ex T, U being abs (ar b₁) -element Element of (AllTermsOf S) * st
( s is operational & seqt `1 = { ((<*(TheEqSymbOf S)*> ^ (TT . j)) ^ (UU . j)) where j is Element of Seg (abs (ar s)), TT, UU is Function of (Seg (abs (ar s))),(((AllSymbolsOf S) *) \ {{}}) : ( TT = T & UU = U ) } & seqt `2 = (<*(TheEqSymbOf S)*> ^ (s -compound T)) ^ (s -compound U) ) by Def23;
then seqt Rule3d Seqts2 by Def23;
then [Seqts2,seqt] in P#3d S by Def36;
hence x in (R#3d S) . Seqts2 by Lm26; :: thesis: verum

end;

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

end;

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