set I = { x where x is Element of V : ( x in conv A & ( for B being Subset of V holds

( not B c< A or not x in conv B ) ) ) } ;

( not B c< A or not x in conv B ) ) ) } as Subset of V by TARSKI:def 3;

take I ; :: thesis: for x being set holds

( x in I iff ( x in conv A & ( for B being Subset of V holds

( not B c< A or not x in conv B ) ) ) )

let x be set ; :: thesis: ( x in I iff ( x in conv A & ( for B being Subset of V holds

( not B c< A or not x in conv B ) ) ) )

( not B c< A or not x in conv B ) ) ) ; :: thesis: x in I

hence x in I ; :: thesis: verum

( not B c< A or not x in conv B ) ) ) } ;

now :: thesis: for x being object st x in { x where x is Element of V : ( x in conv A & ( for B being Subset of V holds

( not B c< A or not x in conv B ) ) ) } holds

x in the carrier of V

then reconsider I = { x where x is Element of V : ( x in conv A & ( for B being Subset of V holds ( not B c< A or not x in conv B ) ) ) } holds

x in the carrier of V

let x be object ; :: thesis: ( x in { x where x is Element of V : ( x in conv A & ( for B being Subset of V holds

( not B c< A or not x in conv B ) ) ) } implies x in the carrier of V )

assume x in { x where x is Element of V : ( x in conv A & ( for B being Subset of V holds

( not B c< A or not x in conv B ) ) ) } ; :: thesis: x in the carrier of V

then ex y being Element of V st

( x = y & y in conv A & ( for B being Subset of V holds

( not B c< A or not y in conv B ) ) ) ;

hence x in the carrier of V ; :: thesis: verum

end;( not B c< A or not x in conv B ) ) ) } implies x in the carrier of V )

assume x in { x where x is Element of V : ( x in conv A & ( for B being Subset of V holds

( not B c< A or not x in conv B ) ) ) } ; :: thesis: x in the carrier of V

then ex y being Element of V st

( x = y & y in conv A & ( for B being Subset of V holds

( not B c< A or not y in conv B ) ) ) ;

hence x in the carrier of V ; :: thesis: verum

( not B c< A or not x in conv B ) ) ) } as Subset of V by TARSKI:def 3;

take I ; :: thesis: for x being set holds

( x in I iff ( x in conv A & ( for B being Subset of V holds

( not B c< A or not x in conv B ) ) ) )

let x be set ; :: thesis: ( x in I iff ( x in conv A & ( for B being Subset of V holds

( not B c< A or not x in conv B ) ) ) )

hereby :: thesis: ( x in conv A & ( for B being Subset of V holds

( not B c< A or not x in conv B ) ) implies x in I )

assume
( x in conv A & ( for B being Subset of V holds ( not B c< A or not x in conv B ) ) implies x in I )

assume
x in I
; :: thesis: ( x in conv A & ( for B being Subset of V holds

( not B c< A or not x in conv B ) ) )

then ex y being Element of V st

( x = y & y in conv A & ( for B being Subset of V holds

( not B c< A or not y in conv B ) ) ) ;

hence ( x in conv A & ( for B being Subset of V holds

( not B c< A or not x in conv B ) ) ) ; :: thesis: verum

end;( not B c< A or not x in conv B ) ) )

then ex y being Element of V st

( x = y & y in conv A & ( for B being Subset of V holds

( not B c< A or not y in conv B ) ) ) ;

hence ( x in conv A & ( for B being Subset of V holds

( not B c< A or not x in conv B ) ) ) ; :: thesis: verum

( not B c< A or not x in conv B ) ) ) ; :: thesis: x in I

hence x in I ; :: thesis: verum