defpred S₁[ object ] means ex C being strict MSSubAlgebra of A st
( $1 = C & B is MSSubAlgebra of C );
for X1, X2 being set st ( for x being object holds
( x in X1 iff S₁[x] ) ) & ( for x being object 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 object holds
( x in b₁ iff ex C being strict MSSubAlgebra of A st
( x = C & B is MSSubAlgebra of C ) ) ) & ( for x being object holds
( x in b₂ iff ex C being strict MSSubAlgebra of A st
( x = C & B is MSSubAlgebra of C ) ) ) holds
b₁ = b₂ ; :: thesis: verum