set O = OneStep D;
set Q = S -sequents ;
set IT = { (iter ((OneStep D),mm)) where mm is Element of NAT : verum } ;

now :: thesis: for x being object st x in { (iter ((OneStep D),mm)) where mm is Element of NAT : verum } holds
x in bool [:(bool (S -sequents)),(bool (S -sequents)):]

let x be object ; :: thesis: ( x in { (iter ((OneStep D),mm)) where mm is Element of NAT : verum } implies x in bool [:(bool (S -sequents)),(bool (S -sequents)):] )
assume x in { (iter ((OneStep D),mm)) where mm is Element of NAT : verum } ; :: thesis: x in bool [:(bool (S -sequents)),(bool (S -sequents)):]
then consider mm being Element of NAT such that
A1: x = iter ((OneStep D),mm) ;
x is Relation of (bool (S -sequents)),(bool (S -sequents)) by Lm1, A1;
hence x in bool [:(bool (S -sequents)),(bool (S -sequents)):] ; :: thesis: verum

end;

hence { (iter ((OneStep D),mm)) where mm is Element of NAT : verum } is Subset-Family of [:(bool (S -sequents)),(bool (S -sequents)):] by TARSKI:def 3; :: thesis: verum