set D = K1 \/ K2;
A7: ( 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: 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 )
let f be Function; :: thesis: ( Seqts1 c= Seqts2 & f in K1 \/ K2 implies ex g being Function st
( g in K1 \/ K2 & f . Seqts1 c= g . Seqts2 ) )
set X = Seqts1;
set Y = Seqts2;
assume A8: ( Seqts1 c= Seqts2 & f in K1 \/ K2 ) ; :: thesis: ex g being Function st
( g in K1 \/ K2 & f . Seqts1 c= g . Seqts2 )

per cases ( f in K1 or not f in K1 ) ;

suppose f in K1 ; :: thesis: ex g being Function st
( g in K1 \/ K2 & f . Seqts1 c= g . Seqts2 )

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

end;

suppose not f in K1 ; :: thesis: ex g being Function st
( g in K1 \/ K2 & f . Seqts1 c= g . Seqts2 )

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

end;

end;

end;

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