set IR9 = the InternalRel of (R \~ );
set C = { (x /\ N) where x is Element of Class (EqRel R) : ex y being Element of (R \~ ) st
( x = Class (EqRel R),y & y is_minimal_wrt N,the InternalRel of (R \~ ) ) } ;

now

let x be set ; :: thesis: ( x in { (x /\ N) where x is Element of Class (EqRel R) : ex y being Element of (R \~ ) st
( x = Class (EqRel R),y & y is_minimal_wrt N,the InternalRel of (R \~ ) ) } implies x in bool the carrier of R )
assume x in { (x /\ N) where x is Element of Class (EqRel R) : ex y being Element of (R \~ ) st
( x = Class (EqRel R),y & y is_minimal_wrt N,the InternalRel of (R \~ ) ) } ; :: thesis: x in bool the carrier of R
then ex xx being Element of Class (EqRel R) st
( x = xx /\ N & ex y being Element of (R \~ ) st
( xx = Class (EqRel R),y & y is_minimal_wrt N,the InternalRel of (R \~ ) ) ) ;
hence x in bool the carrier of R ; :: thesis: verum

end;

then reconsider C = { (x /\ N) where x is Element of Class (EqRel R) : ex y being Element of (R \~ ) st
( x = Class (EqRel R),y & y is_minimal_wrt N,the InternalRel of (R \~ ) ) } as Subset-Family of R by TARSKI:def 3;
take C ; :: thesis: for x being set holds
( x in C iff ex y being Element of (R \~ ) st
( y is_minimal_wrt N,the InternalRel of (R \~ ) & x = (Class (EqRel R),y) /\ N ) )
let x be set ; :: thesis: ( x in C iff ex y being Element of (R \~ ) st
( y is_minimal_wrt N,the InternalRel of (R \~ ) & x = (Class (EqRel R),y) /\ N ) )

hereby :: thesis: ( ex y being Element of (R \~ ) st
( y is_minimal_wrt N,the InternalRel of (R \~ ) & x = (Class (EqRel R),y) /\ N ) implies x in C )

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

end;

given y being Element of (R \~ ) such that A1: y is_minimal_wrt N,the InternalRel of (R \~ ) and
A2: x = (Class (EqRel R),y) /\ N ; :: thesis: x in C
reconsider y9 = y as Element of R ;
EqClass (EqRel R),y9 in Class (EqRel R) ;
hence x in C by A1, A2; :: thesis: verum