defpred S₁[ set , Element of S -sequents ] means $2 Rule7 $1;
let IT1, IT2 be Relation of (bool (S -sequents)),(S -sequents); :: thesis: ( ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in IT1 iff seqt Rule7 Seqts ) ) & ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in IT2 iff seqt Rule7 Seqts ) ) implies IT1 = IT2 )
assume A32: for x being Element of bool (S -sequents)
for y being Element of S -sequents holds
( [x,y] in IT1 iff S₁[x,y] ) ; :: thesis: ( ex Seqts being Element of bool (S -sequents) ex seqt being Element of S -sequents st
( ( [Seqts,seqt] in IT2 implies seqt Rule7 Seqts ) implies ( seqt Rule7 Seqts & not [Seqts,seqt] in IT2 ) ) or IT1 = IT2 )
assume A33: for x being Element of bool (S -sequents)
for y being Element of S -sequents holds
( [x,y] in IT2 iff S₁[x,y] ) ; :: thesis: IT1 = IT2
thus IT1 = IT2 from RELSET_1:sch 4(A32, A33); :: thesis: verum