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;
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 ) ) ; :: thesis: (OneStep D1) . Seqts1 c= (OneStep D2) . Seqts2
now :: thesis: 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 ; :: 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
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;
now :: thesis: ex g being Function st
( g in D2 & RR . Seqts1 c= g . Seqts2 )
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 A5, A2; :: 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
A7: ( g in D1 & RR . Seqts1 c= g . Seqts2 ) by A5, A2;
thus ex g being Function st
( g in D2 & RR . Seqts1 c= g . Seqts2 ) by A7, A2; :: thesis: verum
end;
end;
end;
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; :: thesis: verum
end;
hence (OneStep D1) . Seqts1 c= (OneStep D2) . Seqts2 by A1; :: thesis: verum