set Q = S -sequents ;
let IT1, IT2 be Rule of S; :: thesis: ( ( for inseqs being set st inseqs in bool (S -sequents) holds
IT1 . inseqs = { x where x is Element of S -sequents : [inseqs,x] in R } ) & ( for inseqs being set st inseqs in bool (S -sequents) holds
IT2 . inseqs = { x where x is Element of S -sequents : [inseqs,x] in R } ) implies IT1 = IT2 )
deffunc H₁( object ) -> set = { x where x is Element of S -sequents : [$1,x] in R } ;
assume A5: for inseqs being set st inseqs in bool (S -sequents) holds
IT1 . inseqs = H₁(inseqs) ; :: thesis: ( ex inseqs being set st
( inseqs in bool (S -sequents) & not IT2 . inseqs = { x where x is Element of S -sequents : [inseqs,x] in R } ) or IT1 = IT2 )
assume A6: for inseqs being set st inseqs in bool (S -sequents) holds
IT2 . inseqs = H₁(inseqs) ; :: thesis: IT1 = IT2
for x being object st x in bool (S -sequents) holds
IT1 . x = IT2 . x hence IT1 = IT2 by FUNCT_2:12; :: thesis: verum