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 :: thesis: ( not R is empty & ( for x being Element of R holds
( x in it1 iff x is_minimal_in the carrier of R ) ) & ( for x being Element of R holds
( x in it2 iff x is_minimal_in the carrier of R ) ) implies it1 = it2 )

assume that
not R is empty and
A4: for x being Element of R holds
( x in it1 iff x is_minimal_in the carrier of R ) and
A5: for x being Element of R holds
( x in it2 iff x is_minimal_in the carrier of R ) ; :: thesis: it1 = it2
for x being object holds
( x in it1 iff x in it2 ) by A4, A5;
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