set D = K1 \/ K2;
A6: ( K1 c= K1 \/ K2 & K2 c= K1 \/ K2 ) by XBOOLE_1:7;
for Seqts1, Seqts2 being Subset of (S -sequents)
for f being Function st Seqts1 c= Seqts2 & f in K1 \/ K2 holds
ex g being Function st
( g in K1 \/ K2 & f . Seqts1 c= g . Seqts2 )

proof

let Seqts1, Seqts2 be Subset of (S -sequents); :: thesis:
let f be Function; :: thesis:
set X = Seqts1;
set Y = Seqts2;
assume A7: ( Seqts1 c= Seqts2 & f in K1 \/ K2 ) ; :: thesis:

per cases ;

suppose f in K1 ; :: thesis:

then consider g being Function such that
A8: ( g in K1 & f . Seqts1 c= g . Seqts2 ) by A7, Def11;
take g ; :: thesis:
thus ( g in K1 \/ K2 & f . Seqts1 c= g . Seqts2 ) by A8, A6; :: thesis:

end;

suppose not f in K1 ; :: thesis:

then f in K2 by A7, XBOOLE_0:def 3;
then consider g being Function such that
A9: ( g in K2 & f . Seqts1 c= g . Seqts2 ) by A7, Def11;
take g ; :: thesis:
thus ( g in K1 \/ K2 & f . Seqts1 c= g . Seqts2 ) by A9, A6; :: thesis:

end;

end;

end;

hence for b₁ being RuleSet of S st b₁ = K1 \/ K2 holds
b₁ is isotone ; :: thesis: