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
(OneStep D1) . Seqts1 c= (OneStep D2) . 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
(OneStep D1) . Seqts1 c= (OneStep D2) . Seqts2
let Seqts1, Seqts2 be Subset of (S -sequents); :: thesis: ( Seqts1 c= Seqts2 & D1 c= D2 & ( D2 is isotone or D1 is isotone ) implies (OneStep D1) . Seqts1 c= (OneStep D2) . Seqts2 )
set Q = S -sequents ;
set U1 = union D1;
set U2 = union D2;
set O1 = OneStep D1;
set O2 = OneStep D2;
set F1 = { (R .: {Seqts1}) where R is Subset of [:(bool (S -sequents)),(bool (S -sequents)):] : R in D1 } ;
set F2 = { (R .: {Seqts2}) where R is Subset of [:(bool (S -sequents)),(bool (S -sequents)):] : R in D2 } ;
set X1 = Seqts1;
set X2 = Seqts2;
B2: ( (OneStep D1) . Seqts1 = union (union { (R .: {Seqts1}) where R is Subset of [:(bool (S -sequents)),(bool (S -sequents)):] : R in D1 } ) & (OneStep D2) . Seqts2 = union (union { (R .: {Seqts2}) where R is Subset of [:(bool (S -sequents)),(bool (S -sequents)):] : R in D2 } ) ) by Lm13;
assume B1: ( Seqts1 c= Seqts2 & D1 c= D2 & ( D2 is isotone or D1 is isotone ) ) ; :: thesis: (OneStep D1) . Seqts1 c= (OneStep D2) . Seqts2

now

let z be set ; :: thesis: ( z in union (union { (R .: {Seqts1}) where R is Subset of [:(bool (S -sequents)),(bool (S -sequents)):] : R in D1 } ) implies z in union (union { (R .: {Seqts2}) where R is Subset of [:(bool (S -sequents)),(bool (S -sequents)):] : R in D2 } ) )
assume z in union (union { (R .: {Seqts1}) where R is Subset of [:(bool (S -sequents)),(bool (S -sequents)):] : R in D1 } ) ; :: thesis: z in union (union { (R .: {Seqts2}) where R is Subset of [:(bool (S -sequents)),(bool (S -sequents)):] : R in D2 } )
then consider x being set such that
C7: ( z in x & x in union { (R .: {Seqts1}) where R is Subset of [:(bool (S -sequents)),(bool (S -sequents)):] : R in D1 } ) by TARSKI:def 4;
consider X being set such that
C0: ( x in X & X in { (R .: {Seqts1}) where R is Subset of [:(bool (S -sequents)),(bool (S -sequents)):] : R in D1 } ) by C7, TARSKI:def 4;
consider R being Subset of [:(bool (S -sequents)),(bool (S -sequents)):] such that
C1: ( X = R .: {Seqts1} & R in D1 ) by C0;
reconsider RR = R as Rule of S by C1;
( X = Im (RR,Seqts1) & R in D1 & Seqts1 in dom RR ) by C1, Lm4;
then CC4: X = {(RR . Seqts1)} by FUNCT_1:59;

now

per cases ( D2 is isotone or not D2 is isotone ) ;

suppose D2 is isotone ; :: thesis: ex g being Function st
( g in D2 & RR . Seqts1 c= g . Seqts2 )

hence ex g being Function st
( g in D2 & RR . Seqts1 c= g . Seqts2 ) by C1, B1, DefMonotonic2; :: thesis: verum

end;

suppose not D2 is isotone ; :: thesis: ex g being Function st
( g in D2 & RR . Seqts1 c= g . Seqts2 )

then consider g being Function such that
E1: ( g in D1 & RR . Seqts1 c= g . Seqts2 ) by C1, B1, DefMonotonic2;
thus ex g being Function st
( g in D2 & RR . Seqts1 c= g . Seqts2 ) by E1, B1; :: thesis: verum

end;

end;

end;

then consider g being Function such that
C3: ( g in D2 & RR . Seqts1 c= g . Seqts2 ) ;
reconsider Rg = g as Rule of S by C3;
C5: Seqts2 in dom Rg by Lm4;
C6: x c= g . Seqts2 by C3, CC4, C0, TARSKI:def 1;
Im (Rg,Seqts2) in { (R .: {Seqts2}) where R is Subset of [:(bool (S -sequents)),(bool (S -sequents)):] : R in D2 } by C3;
then {(Rg . Seqts2)} in { (R .: {Seqts2}) where R is Subset of [:(bool (S -sequents)),(bool (S -sequents)):] : R in D2 } by C5, FUNCT_1:59;
then {{(Rg . Seqts2)}} c= { (R .: {Seqts2}) where R is Subset of [:(bool (S -sequents)),(bool (S -sequents)):] : R in D2 } by ZFMISC_1:31;
then union {{(g . Seqts2)}} c= union { (R .: {Seqts2}) where R is Subset of [:(bool (S -sequents)),(bool (S -sequents)):] : R in D2 } by ZFMISC_1:77;
then {(g . Seqts2)} c= union { (R .: {Seqts2}) where R is Subset of [:(bool (S -sequents)),(bool (S -sequents)):] : R in D2 } by ZFMISC_1:25;
then union {(g . Seqts2)} c= union (union { (R .: {Seqts2}) where R is Subset of [:(bool (S -sequents)),(bool (S -sequents)):] : R in D2 } ) by ZFMISC_1:77;
then g . Seqts2 c= union (union { (R .: {Seqts2}) where R is Subset of [:(bool (S -sequents)),(bool (S -sequents)):] : R in D2 } ) by ZFMISC_1:25;
then x c= union (union { (R .: {Seqts2}) where R is Subset of [:(bool (S -sequents)),(bool (S -sequents)):] : R in D2 } ) by C6, XBOOLE_1:1;
hence z in union (union { (R .: {Seqts2}) where R is Subset of [:(bool (S -sequents)),(bool (S -sequents)):] : R in D2 } ) by C7; :: thesis: verum

end;

hence (OneStep D1) . Seqts1 c= (OneStep D2) . Seqts2 by B2, TARSKI:def 3; :: thesis: verum