let it1, it2 be Subset of R; :: thesis: ( ( not R is empty & ( for x being Element of R holds
( x in it1 iff x is_minimal_in [#] R ) ) & ( for x being Element of R holds
( x in it2 iff x is_minimal_in [#] R ) ) implies it1 = it2 ) & ( R is empty & it1 = {} & it2 = {} implies it1 = it2 ) )

now

assume that
not R is empty and
A1: for x being Element of R holds
( x in it1 iff x is_minimal_in the carrier of R ) and
A2: for x being Element of R holds
( x in it2 iff x is_minimal_in the carrier of R ) ; :: thesis: it1 = it2

now

let x be set ; :: thesis: ( x in it1 iff x in it2 )

now

assume A3: ( x in it1 or x in it2 ) ; :: thesis: ( x in it1 & x in it2 )
then reconsider x9 = x as Element of R ;
x9 is_minimal_in the carrier of R by A3, A1, A2;
hence ( x in it1 & x in it2 ) by A1, A2; :: thesis: verum

end;

hence ( x in it1 iff x in it2 ) ; :: thesis: verum

end;

hence it1 = it2 by TARSKI:2; :: thesis: verum

end;

hence ( ( not R is empty & ( for x being Element of R holds
( x in it1 iff x is_minimal_in [#] R ) ) & ( for x being Element of R holds
( x in it2 iff x is_minimal_in [#] R ) ) implies it1 = it2 ) & ( R is empty & it1 = {} & it2 = {} implies it1 = it2 ) ) ; :: thesis: verum