now :: thesis: for Seqts1, Seqts2 being Subset of (S -sequents) st Seqts1 c= Seqts2 holds
(R#2 S) . Seqts1 c= (R#2 S) . Seqts2
let Seqts1, Seqts2 be Subset of (S -sequents); :: thesis: ( Seqts1 c= Seqts2 implies (R#2 S) . Seqts1 c= (R#2 S) . Seqts2 )
set X = Seqts1;
set Y = Seqts2;
assume Seqts1 c= Seqts2 ; :: thesis: (R#2 S) . Seqts1 c= (R#2 S) . Seqts2
set R = R#2 S;
set Q = S -sequents ;
now :: thesis: for x being object st x in (R#2 S) . Seqts1 holds
x in (R#2 S) . Seqts2
let x be object ; :: thesis: ( x in (R#2 S) . Seqts1 implies x in (R#2 S) . Seqts2 )
assume A1: x in (R#2 S) . Seqts1 ; :: thesis: x in (R#2 S) . Seqts2
then A2: ( x in S -sequents & [Seqts1,x] in P#2 S ) by Lm30;
reconsider seqt = x as Element of S -sequents by A1;
seqt Rule2 Seqts1 by Def36, A2;
then ( seqt `1 is empty & ex t being termal string of S st seqt `2 = (<*(TheEqSymbOf S)*> ^ t) ^ t ) ;
then seqt Rule2 Seqts2 ;
then [Seqts2,seqt] in P#2 S by Def36;
hence x in (R#2 S) . Seqts2 by Lm27; :: thesis: verum
end;
hence (R#2 S) . Seqts1 c= (R#2 S) . Seqts2 ; :: thesis: verum
end;
hence for b1 being Rule of S st b1 = R#2 S holds
b1 is isotone ; :: thesis: verum