let m be Nat; :: thesis: for S being Language
for D1, D2 being RuleSet of S
for Seqts1, Seqts2 being Subset of (S -sequents) st Seqts1 c= Seqts2 & D1 c= D2 & ( D2 is isotone or D1 is isotone ) holds
((m,D1) -derivables) . Seqts1 c= ((m,D2) -derivables) . Seqts2
let S be Language; :: thesis: for D1, D2 being RuleSet of S
for Seqts1, Seqts2 being Subset of (S -sequents) st Seqts1 c= Seqts2 & D1 c= D2 & ( D2 is isotone or D1 is isotone ) holds
((m,D1) -derivables) . Seqts1 c= ((m,D2) -derivables) . Seqts2
let D1, D2 be RuleSet of S; :: thesis: for Seqts1, Seqts2 being Subset of (S -sequents) st Seqts1 c= Seqts2 & D1 c= D2 & ( D2 is isotone or D1 is isotone ) holds
((m,D1) -derivables) . Seqts1 c= ((m,D2) -derivables) . Seqts2
let Seqts1, Seqts2 be Subset of (S -sequents); :: thesis: ( Seqts1 c= Seqts2 & D1 c= D2 & ( D2 is isotone or D1 is isotone ) implies ((m,D1) -derivables) . Seqts1 c= ((m,D2) -derivables) . Seqts2 )
set O1 = OneStep D1;
set O2 = OneStep D2;
set Q = S -sequents ;
set X1 = Seqts1;
set X2 = Seqts2;
assume A1: ( Seqts1 c= Seqts2 & D1 c= D2 & ( D2 is isotone or D1 is isotone ) ) ; :: thesis: ((m,D1) -derivables) . Seqts1 c= ((m,D2) -derivables) . Seqts2
defpred S1[ Nat] means (($1,D1) -derivables) . Seqts1 c= (($1,D2) -derivables) . Seqts2;
A2: S1[ 0 ]
proof
A3: (iter ((OneStep D1),0)) . Seqts1 = (id (field (OneStep D1))) . Seqts1 by FUNCT_7:68
.= (id (bool (S -sequents))) . Seqts1 by Lm1
.= Seqts1 ;
(iter ((OneStep D2),0)) . Seqts2 = (id (field (OneStep D2))) . Seqts2 by FUNCT_7:68
.= (id (bool (S -sequents))) . Seqts2 by Lm1
.= Seqts2 ;
hence S1[ 0 ] by A3, A1; :: thesis: verum
end;
A4: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
A5: ( Seqts1 in dom (iter ((OneStep D1),n)) & Seqts2 in dom (iter ((OneStep D2),n)) ) by Lm1;
reconsider X11 = ((n,D1) -derivables) . Seqts1, X22 = ((n,D2) -derivables) . Seqts2 as Subset of (S -sequents) ;
assume A6: S1[n] ; :: thesis: S1[n + 1]
A7: (((n + 1),D1) -derivables) . Seqts1 = ((OneStep D1) * (iter ((OneStep D1),n))) . Seqts1 by FUNCT_7:71
.= (OneStep D1) . X11 by A5, FUNCT_1:13 ;
(((n + 1),D2) -derivables) . Seqts2 = ((OneStep D2) * (iter ((OneStep D2),n))) . Seqts2 by FUNCT_7:71
.= (OneStep D2) . X22 by A5, FUNCT_1:13 ;
hence S1[n + 1] by A7, A6, Lm13, A1; :: thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch 2(A2, A4);
 hence ((m,D1) -derivables) . Seqts1 c= ((m,D2) -derivables) . Seqts2 ; :: thesis: verum