defpred S1[ object ] means ex j being set st ( j in J & j indom A & $1 in A . j ); let A1, A2 be set ; :: thesis: ( ( for x being object holds ( x in A1 iff ex j being set st ( j in J & j indom A & x in A . j ) ) ) & ( for x being object holds ( x in A2 iff ex j being set st ( j in J & j indom A & x in A . j ) ) ) implies A1 = A2 ) assume that A5:
for x being object holds ( x in A1 iff ex j being set st ( j in J & j indom A & x in A . j ) )
and A6:
for x being object holds ( x in A2 iff ex j being set st ( j in J & j indom A & x in A . j ) )
; :: thesis: A1 = A2 A7:
for x being object holds ( x in A2 iff S1[x] )
byA6; A8:
for x being object holds ( x in A1 iff S1[x] )
byA5;
A1 = A2
fromXBOOLE_0:sch 2(A8, A7); hence
A1 = A2
; :: thesis: verum