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_maximal_in [#] R ) ) & ( for x being Element of R holds
( x in it2 iff x is_maximal_in [#] R ) ) implies it1 = it2 ) & ( R is empty & it1 = {} & it2 = {} implies it1 = it2 ) )

now

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

now

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

now

assume A12: ( x in it1 or x in it2 ) ; :: thesis: ( x in it1 & x in it2 )
then reconsider x9 = x as Element of R ;
x9 is_maximal_in the carrier of R by A12, A10, A11;
hence ( x in it1 & x in it2 ) by A10, A11; :: thesis: verum

end;

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

end;

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

end;

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