let X1, X2 be set ; :: thesis: ( ( for x being set holds
( x in X1 iff ( x <> a & [x,a] in R ) ) ) & ( for x being set holds
( x in X2 iff ( x <> a & [x,a] in R ) ) ) implies X1 = X2 )
assume that
A4: for b being set holds
( b in X1 iff S₁[b] ) and
A5: for b being set holds
( b in X2 iff S₁[b] ) ; :: thesis: X1 = X2
thus X1 = X2 from XBOOLE_0:sch 2(A4, A5); :: thesis: verum