defpred S1[ set , Element of S -sequents ] means $2 Rule7 $1;
let IT1, IT2 be Relation of (bool (S -sequents)),(S -sequents); ( ( 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 S1[x,y] )
; ( 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 S1[x,y] )
; IT1 = IT2
thus
IT1 = IT2
from RELSET_1:sch 4(A32, A33); verum