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