let S be 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
(OneStep D1) . Seqts1 c= (OneStep D2) . Seqts2
let D1, D2 be 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 Seqts1, Seqts2 be Subset of (S -sequents); ( 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;
A1:
( (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 Lm5;
assume A2:
( Seqts1 c= Seqts2 & D1 c= D2 & ( D2 is isotone or D1 is isotone ) )
; (OneStep D1) . Seqts1 c= (OneStep D2) . Seqts2
now for z being object st z in union (union { (R .: {Seqts1}) where R is Subset of [:(bool (S -sequents)),(bool (S -sequents)):] : R in D1 } ) holds
z in union (union { (R .: {Seqts2}) where R is Subset of [:(bool (S -sequents)),(bool (S -sequents)):] : R in D2 } )let z be
object ;
( 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 } )
;
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 A3:
(
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 A4:
(
x in X &
X in { (R .: {Seqts1}) where R is Subset of [:(bool (S -sequents)),(bool (S -sequents)):] : R in D1 } )
by TARSKI:def 4, A3;
consider R being
Subset of
[:(bool (S -sequents)),(bool (S -sequents)):] such that A5:
(
X = R .: {Seqts1} &
R in D1 )
by A4;
reconsider RR =
R as
Rule of
S by A5;
(
X = Im (
RR,
Seqts1) &
R in D1 &
Seqts1 in dom RR )
by A5, Lm1;
then A6:
X = {(RR . Seqts1)}
by FUNCT_1:59;
then consider g being
Function such that A8:
(
g in D2 &
RR . Seqts1 c= g . Seqts2 )
;
reconsider Rg =
g as
Rule of
S by A8;
A9:
Seqts2 in dom Rg
by Lm1;
A10:
x c= g . Seqts2
by A8, A6, A4, TARSKI:def 1;
Im (
Rg,
Seqts2)
in { (R .: {Seqts2}) where R is Subset of [:(bool (S -sequents)),(bool (S -sequents)):] : R in D2 }
by A8;
then
{(Rg . Seqts2)} in { (R .: {Seqts2}) where R is Subset of [:(bool (S -sequents)),(bool (S -sequents)):] : R in D2 }
by FUNCT_1:59, A9;
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:31, ZFMISC_1:77;
then
{(g . Seqts2)} c= union { (R .: {Seqts2}) where R is Subset of [:(bool (S -sequents)),(bool (S -sequents)):] : R in D2 }
;
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 } )
;
then
x c= union (union { (R .: {Seqts2}) where R is Subset of [:(bool (S -sequents)),(bool (S -sequents)):] : R in D2 } )
by A10, 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 A3;
verum end;
hence
(OneStep D1) . Seqts1 c= (OneStep D2) . Seqts2
by A1; verum