set Q = S -sequents ;
reconsider I = id (bool (S -sequents)) as Rule of S by Lm2;
take I ; :: thesis: I is isotone
thus I is isotone ; :: thesis: verum