defpred S₁[ set ] means ex q, r, s being set st
( $1 = [q,s] & [q,r] in A & [r,s] in B );
let C, D be set ; :: thesis: ( ( for p being set holds
( p in C iff ex q, r, s being set st
( p = [q,s] & [q,r] in A & [r,s] in B ) ) ) & ( for p being set holds
( p in D iff ex q, r, s being set st
( p = [q,s] & [q,r] in A & [r,s] in B ) ) ) implies C = D )
assume that
A10: for p being set holds
( p in C iff S₁[p] ) and
A11: for p being set holds
( p in D iff S₁[p] ) ; :: thesis: C = D
thus C = D from XBOOLE_0:sch 2(A10, A11); :: thesis: verum