let A1, A2 be set ; :: thesis: ( ( for x being object holds
( x in A1 iff ex M being strict feasible MSAlgebra over S st
( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) ) ) & ( for x being object holds
( x in A2 iff ex M being strict feasible MSAlgebra over S st
( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) ) ) implies A1 = A2 )
assume A31: for x being object holds
( x in A1 iff ex M being strict feasible MSAlgebra over S st
( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) ) ; :: thesis: ( ex x being object st
( ( x in A2 implies ex M being strict feasible MSAlgebra over S st
( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) ) implies ( ex M being strict feasible MSAlgebra over S st
( x = M & ( for C being Component of the Sorts of M holds C c= A ) ) & not x in A2 ) ) or A1 = A2 )
assume A32: for x being object holds
( x in A2 iff ex N being strict feasible MSAlgebra over S st
( x = N & ( for C being Component of the Sorts of N holds C c= A ) ) ) ; :: thesis: A1 = A2
A33: A2 c= A1

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in A2 or a in A1 )
assume a in A2 ; :: thesis: a in A1
then ex M being strict feasible MSAlgebra over S st
( a = M & ( for C being Component of the Sorts of M holds C c= A ) ) by A32;
hence a in A1 by A31; :: thesis: verum

end;

A1 c= A2

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in A1 or a in A2 )
assume a in A1 ; :: thesis: a in A2
then ex M being strict feasible MSAlgebra over S st
( a = M & ( for C being Component of the Sorts of M holds C c= A ) ) by A31;
hence a in A2 by A32; :: thesis: verum

end;

hence A1 = A2 by A33, XBOOLE_0:def 10; :: thesis: verum