let X1, X2 be Subset of X; :: thesis: ( ( for x being object holds
( x in X1 iff x is_maximal_wrt X,R ) ) & ( for x being object holds
( x in X2 iff x is_maximal_wrt X,R ) ) implies X1 = X2 )
assume ( ( for y being object holds
( y in X1 iff S₁[y] ) ) & ( for y being object holds
( y in X2 iff S₁[y] ) ) ) ; :: thesis: X1 = X2
then for y being object holds
( y in X1 iff y in X2 ) ;
hence X1 = X2 by TARSKI:2; :: thesis: verum