let S be Language; :: thesis: for R being Rule of S holds
( id (bool (S -sequents)) is Rule of S & ( R = id (bool (S -sequents)) implies R is isotone ) )
let R be Rule of S; :: thesis: ( id (bool (S -sequents)) is Rule of S & ( R = id (bool (S -sequents)) implies R is isotone ) )
set Q = S -sequents ;
reconsider I = id (bool (S -sequents)) as Rule of S by FUNCT_2:8;
id (bool (S -sequents)) = I ;
hence id (bool (S -sequents)) is Rule of S ; :: thesis: ( R = id (bool (S -sequents)) implies R is isotone )

A1: now :: thesis: for Seqts1, Seqts2 being Subset of (S -sequents) st Seqts1 c= Seqts2 holds
I . Seqts1 c= I . Seqts2

let Seqts1, Seqts2 be Subset of (S -sequents); :: thesis: ( Seqts1 c= Seqts2 implies I . Seqts1 c= I . Seqts2 )
A2: ( I . Seqts1 = Seqts1 & I . Seqts2 = Seqts2 ) by FUNCT_1:17;
assume Seqts1 c= Seqts2 ; :: thesis: I . Seqts1 c= I . Seqts2
hence I . Seqts1 c= I . Seqts2 by A2; :: thesis: verum

end;

assume R = id (bool (S -sequents)) ; :: thesis: R is isotone
hence R is isotone by A1, Def9; :: thesis: verum