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

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

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

let x be object ; :: thesis: ( x in (R#3a S) . Seqts1 implies x in (R#3a S) . Seqts2 )
assume A2: x in (R#3a S) . Seqts1 ; :: thesis: x in (R#3a S) . Seqts2
reconsider seqt = x as Element of S -sequents by A2;
[Seqts1,seqt] in P#3a S by A2, Lm30;
then seqt Rule3a Seqts1 by Def37;
then consider t1, t2, t3 being termal string of S such that
A3: seqt = [{((<*(TheEqSymbOf S)*> ^ t1) ^ t2),((<*(TheEqSymbOf S)*> ^ t2) ^ t3)},((<*(TheEqSymbOf S)*> ^ t1) ^ t3)] ;
seqt Rule3a Seqts2 by A3;
then [Seqts2,seqt] in P#3a S by Def37;
hence x in (R#3a S) . Seqts2 by Lm27; :: thesis: verum

end;

hence (R#3a S) . Seqts1 c= (R#3a S) . Seqts2 ; :: thesis: verum

end;

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