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 :: thesis: for x being object st 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 \~) ) } holds
x in bool the carrier of R
let x be object ; :: 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