set IR = the InternalRel of (R \~);
let IT1, IT2 be Subset-Family of R; :: thesis: ( ( for x being set holds
( x in IT1 iff ex y being Element of (R \~) st
( y is_minimal_wrt N, the InternalRel of (R \~) & x = (Class ((EqRel R),y)) /\ N ) ) ) & ( for x being set holds
( x in IT2 iff ex y being Element of (R \~) st
( y is_minimal_wrt N, the InternalRel of (R \~) & x = (Class ((EqRel R),y)) /\ N ) ) ) implies IT1 = IT2 )
assume that
A3: for x being set holds
( x in IT1 iff ex y being Element of (R \~) st
( y is_minimal_wrt N, the InternalRel of (R \~) & x = (Class ((EqRel R),y)) /\ N ) ) and
A4: for x being set holds
( x in IT2 iff ex y being Element of (R \~) st
( y is_minimal_wrt N, the InternalRel of (R \~) & x = (Class ((EqRel R),y)) /\ N ) ) ; :: thesis: IT1 = IT2

now :: thesis: for x being object holds
( ( x in IT1 implies x in IT2 ) & ( x in IT2 implies x in IT1 ) )

let x be object ; :: thesis: ( ( x in IT1 implies x in IT2 ) & ( x in IT2 implies x in IT1 ) )

hereby :: thesis: ( x in IT2 implies x in IT1 )

assume x in IT1 ; :: thesis: x in IT2
then ex y being Element of (R \~) st
( y is_minimal_wrt N, the InternalRel of (R \~) & x = (Class ((EqRel R),y)) /\ N ) by A3;
hence x in IT2 by A4; :: thesis: verum

end;

assume x in IT2 ; :: thesis: x in IT1
then ex y being Element of (R \~) st
( y is_minimal_wrt N, the InternalRel of (R \~) & x = (Class ((EqRel R),y)) /\ N ) by A4;
hence x in IT1 by A3; :: thesis: verum

end;

hence IT1 = IT2 by TARSKI:2; :: thesis: verum