defpred S₁[ set , Element of S -sequents ] means $2 Rule7 $1;
consider R being Relation of (bool (S -sequents)),(S -sequents) such that
A31: for x being Element of bool (S -sequents)
for y being Element of S -sequents holds
( [x,y] in R iff S₁[x,y] ) from RELSET_1:sch 2();
take R ; :: thesis: for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in R iff seqt Rule7 Seqts )
thus for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in R iff seqt Rule7 Seqts ) by A31; :: thesis: verum