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