now

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

now

let x be set ; :: thesis: ( x in (R3a S) . Seqts1 implies x in (R3a S) . Seqts2 )
assume CC0: x in (R3a S) . Seqts1 ; :: thesis: x in (R3a S) . Seqts2
reconsider seqt = x as Element of S -sequents by CC0;
[Seqts1,seqt] in P3a S by CC0, Lm1e;
then seqt Rule3a Seqts1 by DefP3a;
then consider t, t1, t2 being termal string of S, xx being set such that
C1: ( xx in Seqts1 & seqt `1 = (xx `1) \/ {((<*(TheEqSymbOf S)*> ^ t1) ^ t2)} & xx `2 = (<*(TheEqSymbOf S)*> ^ t) ^ t1 & seqt `2 = (<*(TheEqSymbOf S)*> ^ t) ^ t2 ) by Def3a;
seqt Rule3a Seqts2 by Def3a, C1, B0;
then [Seqts2,seqt] in P3a S by DefP3a;
hence x in (R3a S) . Seqts2 by Lm1; :: thesis: verum

end;

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

end;

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