set R = R#1 S;
set Q = S -sequents ;
now :: thesis: for Seqts, Seqts2 being Subset of (S -sequents) st Seqts c= Seqts2 holds
(R#1 S) . Seqts c= (R#1 S) . Seqts2
let Seqts, Seqts2 be Subset of (S -sequents); :: thesis: ( Seqts c= Seqts2 implies (R#1 S) . Seqts c= (R#1 S) . Seqts2 )
set X = Seqts;
set Y = Seqts2;
assume A1: Seqts c= Seqts2 ; :: thesis: (R#1 S) . Seqts c= (R#1 S) . Seqts2
now :: thesis: for x being object st x in (R#1 S) . Seqts holds
x in (R#1 S) . Seqts2
let x be object ; :: thesis: ( x in (R#1 S) . Seqts implies x in (R#1 S) . Seqts2 )
assume A2: x in (R#1 S) . Seqts ; :: thesis: x in (R#1 S) . Seqts2
reconsider seqt = x as Element of S -sequents by A2;
[Seqts,seqt] in P#1 S by A2, Lm30;
then seqt Rule1 Seqts by Def35;
then consider y being set such that
A3: ( y in Seqts & y `1 c= seqt `1 & seqt `2 = y `2 ) ;
seqt Rule1 Seqts2 by A3, A1;
then [Seqts2,seqt] in P#1 S by Def35;
hence x in (R#1 S) . Seqts2 by Th3; :: thesis: verum
end;
hence (R#1 S) . Seqts c= (R#1 S) . Seqts2 ; :: thesis: verum
end;
hence for b1 being Rule of S st b1 = R#1 S holds
b1 is isotone ; :: thesis: verum