now :: thesis: for Seqts1, Seqts2 being Subset of (S -sequents)
for f being Function st Seqts1 c= Seqts2 & f in {M} holds
ex g being Function st
( g in {M} & f . Seqts1 c= g . Seqts2 )

let Seqts1, Seqts2 be Subset of (S -sequents); :: thesis: for f being Function st Seqts1 c= Seqts2 & f in {M} holds
ex g being Function st
( g in {M} & f . Seqts1 c= g . Seqts2 )
let f be Function; :: thesis: ( Seqts1 c= Seqts2 & f in {M} implies ex g being Function st
( g in {M} & f . Seqts1 c= g . Seqts2 ) )
assume A1: ( Seqts1 c= Seqts2 & f in {M} ) ; :: thesis: ex g being Function st
( g in {M} & f . Seqts1 c= g . Seqts2 )
then reconsider F = f as isotone Rule of S by TARSKI:def 1;
take g = f; :: thesis: ( g in {M} & f . Seqts1 c= g . Seqts2 )
thus g in {M} by A1; :: thesis: f . Seqts1 c= g . Seqts2
F . Seqts1 c= F . Seqts2 by A1, Def10;
hence f . Seqts1 c= g . Seqts2 ; :: thesis: verum

end;

hence for b₁ being RuleSet of S st b₁ = {M} holds
b₁ is isotone ; :: thesis: verum