set IR' = 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 consider xx being Element of Class (EqRel R) such that
A1: x = xx /\ N and
ex y being Element of (R \~ ) st
( xx = Class (EqRel R),y & y is_minimal_wrt N,the InternalRel of (R \~ ) ) ;
thus x in bool the carrier of R by A1; :: 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 consider xx being Element of Class (EqRel R) such that
A2: x = xx /\ N and
A3: ex y being Element of (R \~ ) st
( xx = Class (EqRel R),y & y is_minimal_wrt N,the InternalRel of (R \~ ) ) ;
consider y being Element of (R \~ ) such that
A4: xx = Class (EqRel R),y and
A5: y is_minimal_wrt N,the InternalRel of (R \~ ) by A3;
thus ex y being Element of (R \~ ) st
( y is_minimal_wrt N,the InternalRel of (R \~ ) & x = (Class (EqRel R),y) /\ N ) by A2, A4, A5; :: thesis: verum

end;

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