for X1, X2 being set st ( for x being set holds
( x in X1 iff S₁[x] ) ) & ( for x being set holds
( x in X2 iff S₁[x] ) ) holds
X1 = X2 from XBOOLE_0:sch 3();
hence for b₁, b₂ being set st ( for x being set holds
( x in b₁ iff ex op, v being set st
( x = [op,v] & op in the carrier' of S & v in the carrier of S & ex n being Nat ex args being Element of the carrier of S * st
( the Arity of S . op = args & n in dom args & args . n = v ) ) ) ) & ( for x being set holds
( x in b₂ iff ex op, v being set st
( x = [op,v] & op in the carrier' of S & v in the carrier of S & ex n being Nat ex args being Element of the carrier of S * st
( the Arity of S . op = args & n in dom args & args . n = v ) ) ) ) holds
b₁ = b₂ ; :: thesis: verum