defpred S1[ set , Element of S -sequents ] means $2 Rule1 $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 Rule1 Seqts ) ) & ( for Seqts being Element of bool (S -sequents)
for seqt being Element of S -sequents holds
( [Seqts,seqt] in IT2 iff seqt Rule1 Seqts ) ) implies IT1 = IT2 )
assume A5:
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 Rule1 Seqts ) implies ( seqt Rule1 Seqts & not [Seqts,seqt] in IT2 ) ) or IT1 = IT2 )
assume A6:
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(A5, A6); verum