now

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

now

let x be set ; :: thesis: ( x in (R2 S) . Seqts1 implies x in (R2 S) . Seqts2 )
assume CC0: x in (R2 S) . Seqts1 ; :: thesis: x in (R2 S) . Seqts2
then C0: ( x in S -sequents & [Seqts1,x] in P2 S ) by Lm1e;
reconsider seqt = x as Element of S -sequents by CC0;
seqt Rule2 Seqts1 by DefP2, C0;
then ( seqt `1 is empty & ex t being termal string of S st seqt `2 = (<*(TheEqSymbOf S)*> ^ t) ^ t ) by Def2;
then seqt Rule2 Seqts2 by Def2;
then [Seqts2,seqt] in P2 S by DefP2;
hence x in (R2 S) . Seqts2 by Lm1; :: thesis: verum

end;

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

end;

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